Theorem mp_hswap_thm ≪ | index | src | ≫

MP公式调换形式

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

Step	Hyp	Ref	Expression
1		imp_imp_swapl	((A \imp B) \imp A \imp B) \imp A \imp (A \imp B) \imp B
2		mp_thm	(A \imp B) \imp A \imp B
3	1, 2	ax_mp	A \imp (A \imp B) \imp B

Axiom use

Logic (ax_mp, ax_1, ax_2)