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

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

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