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

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

Proof of Theorem andir
StepHypRef Expression
1 andi 1007 . 2 ((𝜒 ∧ (𝜑𝜓)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
2 ancom 462 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑𝜓)))
3 ancom 462 . . 3 ((𝜑𝜒) ↔ (𝜒𝜑))
4 ancom 462 . . 3 ((𝜓𝜒) ↔ (𝜒𝜓))
53, 4orbi12i 914 . 2 (((𝜑𝜒) ∨ (𝜓𝜒)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
61, 2, 53bitr4i 303 1 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∨ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wo 846
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 206  df-an 398  df-or 847
This theorem is referenced by:  anddi  1010  cases  1042  cador  1610  rexun  4189  rabun2  4312  reuun2  4313  uniprg  4924  xpundir  5743  coundi  6243  mptun  6693  frxp2  8125  tpostpos  8226  ssfi  9169  wemapsolem  9541  ltxr  13091  hashbclem  14407  hashf1lem2  14413  pythagtriplem2  16746  pythagtrip  16763  vdwapun  16903  nosep2o  27165  legtrid  27822  colinearalg  28148  vtxdun  28718  rmoun  31712  elimifd  31753  satfvsuclem2  34289  satf0  34301  dfon2lem5  34697  seglelin  35026  bj-prmoore  35934  wl-ifp4impr  36286  wl-df4-3mintru2  36306  poimirlem30  36456  poimirlem31  36457  cnambfre  36474  expdioph  41695  dflim5  42012  rp-isfinite6  42202  uneqsn  42709
  Copyright terms: Public domain W3C validator