![]() |
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 1007 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓))) | |
2 | ancom 462 | . 2 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑 ∨ 𝜓))) | |
3 | ancom 462 | . . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜑)) | |
4 | ancom 462 | . . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) | |
5 | 3, 4 | orbi12i 914 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓))) |
6 | 1, 2, 5 | 3bitr4i 303 | 1 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∨ wo 846 |
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 206 df-an 398 df-or 847 |
This theorem is referenced by: anddi 1010 cases 1042 cador 1610 rexun 4189 rabun2 4312 reuun2 4313 uniprg 4924 xpundir 5743 coundi 6243 mptun 6693 frxp2 8125 tpostpos 8226 ssfi 9169 wemapsolem 9541 ltxr 13091 hashbclem 14407 hashf1lem2 14413 pythagtriplem2 16746 pythagtrip 16763 vdwapun 16903 nosep2o 27165 legtrid 27822 colinearalg 28148 vtxdun 28718 rmoun 31712 elimifd 31753 satfvsuclem2 34289 satf0 34301 dfon2lem5 34697 seglelin 35026 bj-prmoore 35934 wl-ifp4impr 36286 wl-df4-3mintru2 36306 poimirlem30 36456 poimirlem31 36457 cnambfre 36474 expdioph 41695 dflim5 42012 rp-isfinite6 42202 uneqsn 42709 |
Copyright terms: Public domain | W3C validator |