Theorem imp_introlsl_and ≪ | index | src | ≫

\imp左左\and引入

theorem imp_introlsl_and (A B C: wff): $ (B \imp C) \imp A \and B \imp C $;
StepHypRefExpression
1 imp_introrevr_imp 
(A \and B \imp B) \imp (B \imp C) \imp A \and B \imp C
2 and_splitr 
A \and B \imp B
3 1, 2 ax_mp 
(B \imp C) \imp A \and B \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2, ax_3)