→对→右逆引入
theorem iirvi (A B C: wff): $ (A \imp B) \imp (B \imp C) \imp A \imp C $;
Step | Hyp | Ref | Expression |
---|---|---|---|
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 |