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

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

Proof of Theorem andir
StepHypRef Expression
1 andi 1009 . 2 ((𝜒 ∧ (𝜑𝜓)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
2 ancom 460 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑𝜓)))
3 ancom 460 . . 3 ((𝜑𝜒) ↔ (𝜒𝜑))
4 ancom 460 . . 3 ((𝜓𝜒) ↔ (𝜒𝜓))
53, 4orbi12i 914 . 2 (((𝜑𝜒) ∨ (𝜓𝜒)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
61, 2, 53bitr4i 303 1 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∨ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wo 847
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 848
This theorem is referenced by:  anddi  1012  cases  1042  cador  1609  rexun  4147  rabun2  4275  reuun2  4276  uniprg  4876  xpundir  5691  coundi  6202  mptun  6635  frxp2  8083  tpostpos  8185  ssfi  9092  wemapsolem  9446  ltxr  13024  hashbclem  14369  hashf1lem2  14373  pythagtriplem2  16739  pythagtrip  16756  vdwapun  16896  nosep2o  27631  legtrid  28579  colinearalg  28899  vtxdun  29471  rmoun  32484  elimifd  32534  satfvsuclem2  35415  satf0  35427  dfon2lem5  35840  seglelin  36171  bj-prmoore  37170  wl-ifp4impr  37522  wl-df4-3mintru2  37542  poimirlem30  37700  poimirlem31  37701  cnambfre  37718  fimgmcyclem  42641  expdioph  43130  dflim5  43436  rp-isfinite6  43625  uneqsn  44132
  Copyright terms: Public domain W3C validator