| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > andir | Structured version Visualization version GIF version | ||
| Description: Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.) |
| Ref | Expression |
|---|---|
| andir | ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | andi 1010 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓))) | |
| 2 | ancom 460 | . 2 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑 ∨ 𝜓))) | |
| 3 | ancom 460 | . . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜑)) | |
| 4 | ancom 460 | . . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) | |
| 5 | 3, 4 | orbi12i 915 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓))) |
| 6 | 1, 2, 5 | 3bitr4i 303 | 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: anddi 1013 cases 1043 cador 1608 rexun 4196 rabun2 4324 reuun2 4325 uniprg 4923 xpundir 5755 coundi 6267 mptun 6714 frxp2 8169 tpostpos 8271 ssfi 9213 wemapsolem 9590 ltxr 13157 hashbclem 14491 hashf1lem2 14495 pythagtriplem2 16855 pythagtrip 16872 vdwapun 17012 nosep2o 27727 legtrid 28599 colinearalg 28925 vtxdun 29499 rmoun 32513 elimifd 32556 satfvsuclem2 35365 satf0 35377 dfon2lem5 35788 seglelin 36117 bj-prmoore 37116 wl-ifp4impr 37468 wl-df4-3mintru2 37488 poimirlem30 37657 poimirlem31 37658 cnambfre 37675 fimgmcyclem 42543 expdioph 43035 dflim5 43342 rp-isfinite6 43531 uneqsn 44038 |
| Copyright terms: Public domain | W3C validator |