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 1001 | . 2 ⊢ ((𝜒 ∧ (𝜑 ∨ 𝜓)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓))) | |
2 | ancom 461 | . 2 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑 ∨ 𝜓))) | |
3 | ancom 461 | . . 3 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜑)) | |
4 | ancom 461 | . . 3 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) | |
5 | 3, 4 | orbi12i 908 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒)) ↔ ((𝜒 ∧ 𝜑) ∨ (𝜒 ∧ 𝜓))) |
6 | 1, 2, 5 | 3bitr4i 304 | 1 ⊢ (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 ∨ wo 841 |
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 208 df-an 397 df-or 842 |
This theorem is referenced by: anddi 1004 cases 1034 cador 1600 rexun 4163 rabun2 4279 reuun2 4283 xpundir 5614 coundi 6093 mptun 6487 tpostpos 7901 wemapsolem 9002 ltxr 12498 hashbclem 13798 hashf1lem2 13802 pythagtriplem2 16142 pythagtrip 16159 vdwapun 16298 legtrid 26304 colinearalg 26623 vtxdun 27190 rmoun 30185 elimifd 30225 satfvsuclem2 32504 satf0 32516 dfon2lem5 32929 seglelin 33474 poimirlem30 34803 poimirlem31 34804 cnambfre 34821 expdioph 39498 rp-isfinite6 39762 uneqsn 40251 |
Copyright terms: Public domain | W3C validator |