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