Theorem fomp ≪ | index | src | ≫

$\fo$ 的MP规则

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

Step	Hyp	Ref	Expression
1		hyp h1	\fo x A \imp B
2		hyp h2	A
3	2	intro_fo	\fo x A
4	1, 3	ax_mp	B

Axiom use

Logic (ax_mp, ax_gen)