\imp\iff左分配
theorem imp_iff_distl (A B C: wff): $ A \imp (B \iff C) \iff A \imp B \iff A \imp C $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_comp | ((A \imp (B \iff C)) \imp (A \imp B \iff A \imp C)) \imp ((A \imp B \iff A \imp C) \imp A \imp (B \iff C)) \imp (A \imp (B \iff C) \iff A \imp B \iff A \imp C) |
|
| 2 | imp_iff_insl | (A \imp (B \iff C)) \imp (A \imp B \iff A \imp C) |
|
| 3 | 1, 2 | ax_mp | ((A \imp B \iff A \imp C) \imp A \imp (B \iff C)) \imp (A \imp (B \iff C) \iff A \imp B \iff A \imp C) |
| 4 | imp_iff_extl | (A \imp B \iff A \imp C) \imp A \imp (B \iff C) |
|
| 5 | 3, 4 | ax_mp | A \imp (B \iff C) \iff A \imp B \iff A \imp C |