| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > anddi | Structured version Visualization version GIF version | ||
| Description: Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.) |
| Ref | Expression |
|---|---|
| anddi | ⊢ (((𝜑 ∨ 𝜓) ∧ (𝜒 ∨ 𝜃)) ↔ (((𝜑 ∧ 𝜒) ∨ (𝜑 ∧ 𝜃)) ∨ ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃)))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | andir 1011 | . 2 ⊢ (((𝜑 ∨ 𝜓) ∧ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∧ (𝜒 ∨ 𝜃)) ∨ (𝜓 ∧ (𝜒 ∨ 𝜃)))) | |
| 2 | andi 1010 | . . 3 ⊢ ((𝜑 ∧ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜑 ∧ 𝜃))) | |
| 3 | andi 1010 | . . 3 ⊢ ((𝜓 ∧ (𝜒 ∨ 𝜃)) ↔ ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃))) | |
| 4 | 2, 3 | orbi12i 915 | . 2 ⊢ (((𝜑 ∧ (𝜒 ∨ 𝜃)) ∨ (𝜓 ∧ (𝜒 ∨ 𝜃))) ↔ (((𝜑 ∧ 𝜒) ∨ (𝜑 ∧ 𝜃)) ∨ ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃)))) |
| 5 | 1, 4 | bitri 275 | 1 ⊢ (((𝜑 ∨ 𝜓) ∧ (𝜒 ∨ 𝜃)) ↔ (((𝜑 ∧ 𝜒) ∨ (𝜑 ∧ 𝜃)) ∨ ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃)))) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 ∨ wo 848 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 |
| This theorem is referenced by: prnebg 4856 funun 6612 addsproplem2 28003 mulsproplem9 28150 disjxpin 32601 icoreclin 37358 undif3VD 44902 |
| Copyright terms: Public domain | W3C validator |