Theorem _hyp_imp_intrors_fo_nfls ≪ | index | src | ≫

imp_intrors_fo_nfls的假设和公式无关形式（不可引用）

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

Step	Hyp	Ref	Expression
1		imp_repsecond	(G \imp \fo x A \imp \fo x B) \imp (A \imp \fo x A) \imp G \imp A \imp \fo x B
2		hyp g	\nf x G
3		hyp h	G \imp A \imp B
4	2, 3	_hyp_imp_intro_fo	G \imp \fo x A \imp \fo x B
5	1, 4	ax_mp	(A \imp \fo x A) \imp G \imp A \imp \fo x B
6		hyp n	\nf x A
7	6	fo_intro_nf	A \imp \fo x A
8	5, 7	ax_mp	G \imp A \imp \fo x B

Axiom use

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