Theorem imp_assocfwd ≪ | index | src | ≫

\imp正结合

theorem imp_assocfwd (A B C: wff): $ ((A \imp B) \imp C) \imp A \imp B \imp C $;

Step	Hyp	Ref	Expression
1		imp_introrsl_imp	(((A \imp B) \imp C) \imp B \imp C) \imp ((A \imp B) \imp C) \imp A \imp B \imp C
2		imp_introrevr_imp	(B \imp A \imp B) \imp ((A \imp B) \imp C) \imp B \imp C
3		introl_imp	B \imp A \imp B
4	2, 3	ax_mp	((A \imp B) \imp C) \imp B \imp C
5	1, 4	ax_mp	((A \imp B) \imp C) \imp A \imp B \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2)