Theorem imp_intrors_fo_nfls ≪ | index | src | ≫

\imp右侧引入\fo(左侧无关)

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

Step	Hyp	Ref	Expression
1		imp_tran	(A \imp \fo x A) \imp (\fo x A \imp \fo x B) \imp A \imp \fo x B
2		hyp n	\nf x A
3	2	_nf_decomp	A \imp \fo x A
4	1, 3	ax_mp	(\fo x A \imp \fo x B) \imp A \imp \fo x B
5		hyp h	A \imp B
6	5	imp_intro_fo	\fo x A \imp \fo x B
7	4, 6	ax_mp	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)