\or\imp右分配\and
theorem or_imp_distr_and (A B C: wff): $ A \or B \imp C \iff (A \imp C) \and (B \imp C) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_comp | ((A \or B \imp C) \imp (A \imp C) \and (B \imp C)) \imp ((A \imp C) \and (B \imp C) \imp A \or B \imp C) \imp (A \or B \imp C \iff (A \imp C) \and (B \imp C)) |
|
| 2 | or_imp_insr_and | (A \or B \imp C) \imp (A \imp C) \and (B \imp C) |
|
| 3 | 1, 2 | ax_mp | ((A \imp C) \and (B \imp C) \imp A \or B \imp C) \imp (A \or B \imp C \iff (A \imp C) \and (B \imp C)) |
| 4 | imp_and_extr_or | (A \imp C) \and (B \imp C) \imp A \or B \imp C |
|
| 5 | 3, 4 | ax_mp | A \or B \imp C \iff (A \imp C) \and (B \imp C) |