Theorem imp_for_imp_left_intro ≪ | index | src | ≫

→对→左引入

theorem imp_for_imp_left_intro (A B C: wff):
  $ (B \imp C) \imp (A \imp B) \imp A \imp C $;
StepHypRefExpression
1 imp_for_imp_left_insert 
((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 imp_left_intro 
((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_for_imp_left_insert 
(A \imp B \imp C) \imp (A \imp B) \imp A \imp C
4 2, 3 mp 
(B \imp C) \imp (A \imp B \imp C) \imp (A \imp B) \imp A \imp C
5 1, 4 mp 
((B \imp C) \imp A \imp B \imp C) \imp (B \imp C) \imp (A \imp B) \imp A \imp C
6 imp_left_intro 
(B \imp C) \imp A \imp B \imp C
7 5, 6 mp 
(B \imp C) \imp (A \imp B) \imp A \imp C

Axiom use

ZFC (ax_mp, ax_p1, ax_p2)