\imp\iff左插入
theorem imp_iff_insl (A B C: wff): $ (A \imp (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 | (A \imp (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_imp_insl | (A \imp B \imp C) \imp (A \imp B) \imp A \imp C |
|
| 4 | 3 | _hyp_null_complete | (A \imp (B \iff C)) \imp (A \imp B \imp C) \imp (A \imp B) \imp A \imp C |
| 5 | imp_and_splitrsl | (A \imp (B \imp C) \and (C \imp B)) \imp A \imp B \imp C |
|
| 6 | 5 | _hyp_null_complete | (A \imp (B \iff C)) \imp (A \imp (B \imp C) \and (C \imp B)) \imp A \imp B \imp C |
| 7 | _hyp_null_intro | (A \imp (B \iff C)) \imp A \imp (B \iff C) |
|
| 8 | 7 | conv iff | (A \imp (B \iff C)) \imp A \imp (B \imp C) \and (C \imp B) |
| 9 | 6, 8 | _hyp_mp | (A \imp (B \iff C)) \imp A \imp B \imp C |
| 10 | 4, 9 | _hyp_mp | (A \imp (B \iff C)) \imp (A \imp B) \imp A \imp C |
| 11 | 2, 10 | _hyp_mp | (A \imp (B \iff C)) \imp ((A \imp C) \imp A \imp B) \imp (A \imp B \iff A \imp C) |
| 12 | imp_imp_insl | (A \imp C \imp B) \imp (A \imp C) \imp A \imp B |
|
| 13 | 12 | _hyp_null_complete | (A \imp (B \iff C)) \imp (A \imp C \imp B) \imp (A \imp C) \imp A \imp B |
| 14 | imp_and_splitrsr | (A \imp (B \imp C) \and (C \imp B)) \imp A \imp C \imp B |
|
| 15 | 14 | _hyp_null_complete | (A \imp (B \iff C)) \imp (A \imp (B \imp C) \and (C \imp B)) \imp A \imp C \imp B |
| 16 | 15, 8 | _hyp_mp | (A \imp (B \iff C)) \imp A \imp C \imp B |
| 17 | 13, 16 | _hyp_mp | (A \imp (B \iff C)) \imp (A \imp C) \imp A \imp B |
| 18 | 11, 17 | _hyp_mp | (A \imp (B \iff C)) \imp (A \imp B \iff A \imp C) |