\or\and右分配
theorem or_and_distr (A B C: wff): $ A \or B \and C \iff A \and C \or (B \and C) $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iff_tran | (A \or B \and C \iff C \and A \or (C \and B)) \imp (C \and A \or (C \and B) \iff A \and C \or (B \and C)) \imp (A \or B \and C \iff A \and C \or (B \and C)) |
|
| 2 | iff_tran | (A \or B \and C \iff C \and (A \or B)) \imp (C \and (A \or B) \iff C \and A \or (C \and B)) \imp (A \or B \and C \iff C \and A \or (C \and B)) |
|
| 3 | and_comm | A \or B \and C \iff C \and (A \or B) |
|
| 4 | 2, 3 | ax_mp | (C \and (A \or B) \iff C \and A \or (C \and B)) \imp (A \or B \and C \iff C \and A \or (C \and B)) |
| 5 | and_or_distl | C \and (A \or B) \iff C \and A \or (C \and B) |
|
| 6 | 4, 5 | ax_mp | A \or B \and C \iff C \and A \or (C \and B) |
| 7 | 1, 6 | ax_mp | (C \and A \or (C \and B) \iff A \and C \or (B \and C)) \imp (A \or B \and C \iff A \and C \or (B \and C)) |
| 8 | iff_simintro_or | (C \and A \iff A \and C) \imp (C \and B \iff B \and C) \imp (C \and A \or (C \and B) \iff A \and C \or (B \and C)) |
|
| 9 | and_comm | C \and A \iff A \and C |
|
| 10 | 8, 9 | ax_mp | (C \and B \iff B \and C) \imp (C \and A \or (C \and B) \iff A \and C \or (B \and C)) |
| 11 | and_comm | C \and B \iff B \and C |
|
| 12 | 10, 11 | ax_mp | C \and A \or (C \and B) \iff A \and C \or (B \and C) |
| 13 | 7, 12 | ax_mp | A \or B \and C \iff A \and C \or (B \and C) |