\iff\imp传递至\imp
theorem iff_imp_tran_imp (A B C: wff): $ (A \iff B) \imp (B \imp C) \imp A \imp C $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp_tran | (A \imp B) \imp (B \imp C) \imp A \imp C |
|
| 2 | 1 | _hyp_null_complete | (A \iff B) \and (B \imp C) \imp (A \imp B) \imp (B \imp C) \imp A \imp C |
| 3 | iff_decomp | (A \iff B) \imp A \imp B |
|
| 4 | 3 | _hyp_null_complete | (A \iff B) \and (B \imp C) \imp (A \iff B) \imp A \imp B |
| 5 | _hyp_null_intro | (A \iff B) \imp (A \iff B) |
|
| 6 | 5 | _hyp_complete | (A \iff B) \and (B \imp C) \imp (A \iff B) |
| 7 | 4, 6 | _hyp_mp | (A \iff B) \and (B \imp C) \imp A \imp B |
| 8 | 2, 7 | _hyp_mp | (A \iff B) \and (B \imp C) \imp (B \imp C) \imp A \imp C |
| 9 | _hyp_intro | (A \iff B) \and (B \imp C) \imp B \imp C |
|
| 10 | 8, 9 | _hyp_mp | (A \iff B) \and (B \imp C) \imp A \imp C |
| 11 | 10 | _hyp_rm | (A \iff B) \imp (B \imp C) \imp A \imp C |