Theorem imp_introl_or ≪ | index | src | ≫

\or对\imp左引入

theorem imp_introl_or (A B C: wff): $ (A \imp B) \imp C \or A \imp C \or B $;
StepHypRefExpression
1 imp_introl_imp 
(A \imp B) \imp (\neg C \imp A) \imp \neg C \imp B
2 1 conv or 
(A \imp B) \imp C \or A \imp C \or B

Axiom use

Logic (ax_mp, ax_1, ax_2)