MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  andir Structured version   Visualization version   GIF version

Theorem andir 1002
Description: Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
Assertion
Ref Expression
andir (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∨ (𝜓𝜒)))

Proof of Theorem andir
StepHypRef Expression
1 andi 1001 . 2 ((𝜒 ∧ (𝜑𝜓)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
2 ancom 461 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑𝜓)))
3 ancom 461 . . 3 ((𝜑𝜒) ↔ (𝜒𝜑))
4 ancom 461 . . 3 ((𝜓𝜒) ↔ (𝜒𝜓))
53, 4orbi12i 908 . 2 (((𝜑𝜒) ∨ (𝜓𝜒)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
61, 2, 53bitr4i 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