Theorem _hyp_imp_introls_ex_nfrs ≪ | index | src | ≫

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

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

Step	Hyp	Ref	Expression
1		imp_tran	(G \imp \neg B \imp \fo x \neg A) \imp ((\neg B \imp \fo x \neg A) \imp \ex x A \imp B) \imp G \imp \ex x A \imp B
2		hyp g	\nf x G
3		hyp n	\nf x B
4	3	_nf_clos_neg	\nf x \neg B
5		imp_tran	(G \imp A \imp B) \imp ((A \imp B) \imp \neg B \imp \neg A) \imp G \imp \neg B \imp \neg A
6		hyp h	G \imp A \imp B
7	5, 6	ax_mp	((A \imp B) \imp \neg B \imp \neg A) \imp G \imp \neg B \imp \neg A
8		imp_introrev_neg	(A \imp B) \imp \neg B \imp \neg A
9	7, 8	ax_mp	G \imp \neg B \imp \neg A
10	2, 4, 9	_hyp_imp_intrors_fo_nfls	G \imp \neg B \imp \fo x \neg A
11	1, 10	ax_mp	((\neg B \imp \fo x \neg A) \imp \ex x A \imp B) \imp G \imp \ex x A \imp B
12		neg_imp_swap	(\neg B \imp \fo x \neg A) \imp \neg \fo x \neg A \imp B
13	12	conv ex	(\neg B \imp \fo x \neg A) \imp \ex x A \imp B
14	11, 13	ax_mp	G \imp \ex x A \imp B

Axiom use

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