Theorem imp_introl_imp ≪ | index | src | ≫

\imp左引入\imp

theorem imp_introl_imp (A B C: wff):
  $ (B \imp C) \imp (A \imp B) \imp A \imp C $;
StepHypRefExpression
1 imp_imp_insl 
((B \imp C) \imp (A \imp B \imp C) \imp (A \imp B) \imp A \imp C) \imp ((B \imp C) \imp A \imp B \imp C) \imp (B \imp C) \imp (A \imp B) \imp A \imp C
2 introl_imp 
((A \imp B \imp C) \imp (A \imp B) \imp A \imp C) \imp (B \imp C) \imp (A \imp B \imp C) \imp (A \imp B) \imp A \imp C
3 imp_imp_insl 
(A \imp B \imp C) \imp (A \imp B) \imp A \imp C
4 2, 3 ax_mp 
(B \imp C) \imp (A \imp B \imp C) \imp (A \imp B) \imp A \imp C
5 1, 4 ax_mp 
((B \imp C) \imp A \imp B \imp C) \imp (B \imp C) \imp (A \imp B) \imp A \imp C
6 introl_imp 
(B \imp C) \imp A \imp B \imp C
7 5, 6 ax_mp 
(B \imp C) \imp (A \imp B) \imp A \imp C

Axiom use

Logic (ax_mp, ax_1, ax_2)