Theorem _hyp_intro_fo ≪ | index | src | ≫

intro_fo的假设无关形式（不可引用）

theorem _hyp_intro_fo {x: set} (G A: wff x):
  $ \nf x G $ >
  $ G \imp A $ >
  $ G \imp \fo x A $;

Step	Hyp	Ref	Expression
1		hyp g	\nf x G
2		hyp h	G \imp A
3	1, 2	imp_intrors_fo_nfls	G \imp \fo x A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_5, ax_6, ax_7, ax_12)