Theorem _nf_comp ≪ | index | src | ≫

\nf合成（不可引用）

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

Step	Hyp	Ref	Expression
1		imp_replast	(\fo x (A \imp \fo x A) \imp \ex x A \imp \ex x \fo x A) \imp (\ex x \fo x A \imp \fo x A) \imp \fo x (A \imp \fo x A) \imp \ex x A \imp \fo x A
2		fo_imp_insto_ex	\fo x (A \imp \fo x A) \imp \ex x A \imp \ex x \fo x A
3	1, 2	ax_mp	(\ex x \fo x A \imp \fo x A) \imp \fo x (A \imp \fo x A) \imp \ex x A \imp \fo x A
4		exfo_elim_fo	\ex x \fo x A \imp \fo x A
5	3, 4	ax_mp	\fo x (A \imp \fo x A) \imp \ex x A \imp \fo x A
6		hyp h	A \imp \fo x A
7	6	intro_fo	\fo x (A \imp \fo x A)
8	5, 7	ax_mp	\ex x A \imp \fo x A
9	8	conv nf	\nf x A

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3, ax_gen, ax_4, ax_10)