\iff左引入\imp
theorem iff_introl_imp (A B C: wff): $ (B \iff C) \imp (A \imp B \iff A \imp C) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_comp | ((A \imp B) \imp A \imp C) \imp ((A \imp C) \imp A \imp B) \imp (A \imp B \iff A \imp C) |
|
| 2 | 1 | _hyp_null_complete | (B \iff C) \imp ((A \imp B) \imp A \imp C) \imp ((A \imp C) \imp A \imp B) \imp (A \imp B \iff A \imp C) |
| 3 | imp_introl_imp | (B \imp C) \imp (A \imp B) \imp A \imp C |
|
| 4 | 3 | _hyp_null_complete | (B \iff C) \imp (B \imp C) \imp (A \imp B) \imp A \imp C |
| 5 | iff_decomp | (B \iff C) \imp B \imp C |
|
| 6 | 5 | _hyp_null_complete | (B \iff C) \imp (B \iff C) \imp B \imp C |
| 7 | _hyp_null_intro | (B \iff C) \imp (B \iff C) |
|
| 8 | 6, 7 | _hyp_mp | (B \iff C) \imp B \imp C |
| 9 | 4, 8 | _hyp_mp | (B \iff C) \imp (A \imp B) \imp A \imp C |
| 10 | 2, 9 | _hyp_mp | (B \iff C) \imp ((A \imp C) \imp A \imp B) \imp (A \imp B \iff A \imp C) |
| 11 | imp_introl_imp | (C \imp B) \imp (A \imp C) \imp A \imp B |
|
| 12 | 11 | _hyp_null_complete | (B \iff C) \imp (C \imp B) \imp (A \imp C) \imp A \imp B |
| 13 | iff_decompbwd | (B \iff C) \imp C \imp B |
|
| 14 | 13 | _hyp_null_complete | (B \iff C) \imp (B \iff C) \imp C \imp B |
| 15 | 14, 7 | _hyp_mp | (B \iff C) \imp C \imp B |
| 16 | 12, 15 | _hyp_mp | (B \iff C) \imp (A \imp C) \imp A \imp B |
| 17 | 10, 16 | _hyp_mp | (B \iff C) \imp (A \imp B \iff A \imp C) |