Theorem iirvi | index | src |

→对→右逆引入

theorem iirvi (A B C: wff): $ (A \imp B) \imp (B \imp C) \imp A \imp C $;
StepHypRefExpression
1 iilp
((B \imp C) \imp (A \imp B) \imp A \imp C) \imp (A \imp B) \imp (B \imp C) \imp A \imp C
2 iili
(B \imp C) \imp (A \imp B) \imp A \imp C
3 1, 2 mp
(A \imp B) \imp (B \imp C) \imp A \imp C

Axiom use

ZFC (ax_mp, ax_p1, ax_p2)