Theorem iili ≪ | index | src | ≫

→对→左引入

theorem iili (A B C: wff): $ (B \imp C) \imp (A \imp B) \imp A \imp C $;
StepHypRefExpression
1 iils 
((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 ili 
((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 iils 
(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 ili 
(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)