Theorem mp_thm ≪ | index | src | ≫

MP公式

theorem mp_thm (A B: wff): $ (A \imp B) \imp A \imp B $;

Step	Hyp	Ref	Expression
1		imp_refl	(A \imp B) \imp A \imp B

Axiom use

Logic (ax_mp, ax_1, ax_2)