Theorem mp ≪ | index | src | ≫

MP规则

theorem mp (A B: wff): $ A \imp B $ > $ A $ > $ B $;

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

Axiom use

ZFC (ax_mp)