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

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

Proof of Theorem andir
StepHypRef Expression
1 andi 1008 . 2 ((𝜒 ∧ (𝜑𝜓)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
2 ancom 464 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑𝜓)))
3 ancom 464 . . 3 ((𝜑𝜒) ↔ (𝜒𝜑))
4 ancom 464 . . 3 ((𝜓𝜒) ↔ (𝜒𝜓))
53, 4orbi12i 915 . 2 (((𝜑𝜒) ∨ (𝜓𝜒)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
61, 2, 53bitr4i 306 1 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∨ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  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 210  df-an 400  df-or 848
This theorem is referenced by:  anddi  1011  cases  1043  cador  1615  rexun  4104  rabun2  4228  reuun2  4229  uniprg  4836  xpundir  5618  coundi  6111  mptun  6524  tpostpos  7988  ssfi  8851  wemapsolem  9166  ltxr  12707  hashbclem  14016  hashf1lem2  14022  pythagtriplem2  16370  pythagtrip  16387  vdwapun  16527  legtrid  26682  colinearalg  27001  vtxdun  27569  rmoun  30561  elimifd  30605  satfvsuclem2  33035  satf0  33047  dfon2lem5  33482  frxp2  33528  nosep2o  33622  seglelin  34155  bj-prmoore  35021  wl-ifp4impr  35375  wl-df4-3mintru2  35395  poimirlem30  35544  poimirlem31  35545  cnambfre  35562  expdioph  40548  rp-isfinite6  40810  uneqsn  41310
  Copyright terms: Public domain W3C validator