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 907 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓))) | |
2 | ancom 465 | . 2 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑 ∨ 𝜓))) | |
3 | ancom 465 | . . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜑)) | |
4 | ancom 465 | . . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) | |
5 | 3, 4 | orbi12i 542 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓))) |
6 | 1, 2, 5 | 3bitr4i 291 | 1 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∨ wo 382 ∧ wa 383 |
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 196 df-or 384 df-an 385 |
This theorem is referenced by: anddi 910 cases 1004 cador 1538 rexun 3755 rabun2 3865 reuun2 3869 xpundir 5095 coundi 5553 mptun 5938 tpostpos 7259 wemapsolem 8338 ltxr 11825 hashbclem 13093 hashf1lem2 13097 pythagtriplem2 15360 pythagtrip 15377 vdwapun 15516 legtrid 25286 colinearalg 25590 usgraedg4 25916 vdgrun 26428 vdgrfiun 26429 elimifd 28746 dfon2lem5 30936 nobndup 31099 nofulllem5 31105 seglelin 31393 poimirlem30 32609 poimirlem31 32610 cnambfre 32628 expdioph 36608 rp-isfinite6 36883 uneqsn 37341 vtxdun 40696 |
Copyright terms: Public domain | W3C validator |