Theorem fo_imp_distrs_nfls ≪ | index | src | ≫

\fo\imp分配右侧(左侧无关)

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

Step	Hyp	Ref	Expression
1		iff_comp	(\fo x (A \imp B) \imp A \imp \fo x B) \imp ((A \imp \fo x B) \imp \fo x (A \imp B)) \imp (\fo x (A \imp B) \iff A \imp \fo x B)
2		imp_tran	(\fo x (A \imp B) \imp \fo x A \imp \fo x B) \imp ((\fo x A \imp \fo x B) \imp A \imp \fo x B) \imp \fo x (A \imp B) \imp A \imp \fo x B
3		fo_imp_ins	\fo x (A \imp B) \imp \fo x A \imp \fo x B
4	2, 3	ax_mp	((\fo x A \imp \fo x B) \imp A \imp \fo x B) \imp \fo x (A \imp B) \imp A \imp \fo x B
5		imp_introrevr_imp	(A \imp \fo x A) \imp (\fo x A \imp \fo x B) \imp A \imp \fo x B
6		hyp n	\nf x A
7	6	_nf_decomp	A \imp \fo x A
8	5, 7	ax_mp	(\fo x A \imp \fo x B) \imp A \imp \fo x B
9	4, 8	ax_mp	\fo x (A \imp B) \imp A \imp \fo x B
10	1, 9	ax_mp	((A \imp \fo x B) \imp \fo x (A \imp B)) \imp (\fo x (A \imp B) \iff A \imp \fo x B)
11		imp_tran	((A \imp \fo x B) \imp \ex x A \imp \fo x B) \imp ((\ex x A \imp \fo x B) \imp \fo x (A \imp B)) \imp (A \imp \fo x B) \imp \fo x (A \imp B)
12		imp_introrevr_imp	(\ex x A \imp A) \imp (A \imp \fo x B) \imp \ex x A \imp \fo x B
13	6	ex_elim_nf	\ex x A \imp A
14	12, 13	ax_mp	(A \imp \fo x B) \imp \ex x A \imp \fo x B
15	11, 14	ax_mp	((\ex x A \imp \fo x B) \imp \fo x (A \imp B)) \imp (A \imp \fo x B) \imp \fo x (A \imp B)
16		ex_imp_fo_extto_fo	(\ex x A \imp \fo x B) \imp \fo x (A \imp B)
17	15, 16	ax_mp	(A \imp \fo x B) \imp \fo x (A \imp B)
18	10, 17	ax_mp	\fo x (A \imp B) \iff 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)