Theorem imp_introrsl_imp ≪ | index | src | ≫

\imp左引入右侧

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

Step	Hyp	Ref	Expression
1		imp_introl_imp	(B \imp C \imp B) \imp (A \imp B) \imp A \imp C \imp B
2		introl_imp	B \imp C \imp B
3	1, 2	ax_mp	(A \imp B) \imp A \imp C \imp B

Axiom use

Logic (ax_mp, ax_1, ax_2)