Theorem mpex_nfrs ≪ | index | src | ≫

带\ex的MP规则(无关)

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

Step	Hyp	Ref	Expression
1		hyp n	\nf x B
2		hyp h1	A \imp B
3	1, 2	imp_introls_ex_nfrs	\ex x A \imp B
4		hyp h2	\ex x A
5	3, 4	ax_mp	B

Axiom use

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