Theorem _hyp_mpex_nfrs ≪ | index | src | ≫

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

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

Step	Hyp	Ref	Expression
1		hyp g	\nf x G
2		hyp n	\nf x B
3		hyp h1	G \imp A \imp B
4	1, 2, 3	_hyp_imp_introls_ex_nfrs	G \imp \ex x A \imp B
5		hyp h2	G \imp \ex x A
6	4, 5	_hyp_mp	G \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)