Theorem _nf_decomp ≪ | index | src | ≫

\nf拆解（不可引用）

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

Step	Hyp	Ref	Expression
1		imp_introrevr_imp	(A \imp \ex x A) \imp (\ex x A \imp \fo x A) \imp A \imp \fo x A
2		ex_intro	A \imp \ex x A
3	1, 2	ax_mp	(\ex x A \imp \fo x A) \imp A \imp \fo x A
4	3	conv nf	\nf x A \imp A \imp \fo x A
5		hyp h	\nf x A
6	4, 5	ax_mp	A \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)