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  4148  rabun2  4276  reuun2  4277  uniprg  4879  xpundir  5694  coundi  6205  mptun  6638  frxp2  8086  tpostpos  8188  ssfi  9097  wemapsolem  9455  ltxr  13029  hashbclem  14375  hashf1lem2  14379  pythagtriplem2  16745  pythagtrip  16762  vdwapun  16902  nosep2o  27650  legtrid  28663  colinearalg  28983  vtxdun  29555  rmoun  32568  elimifd  32618  satfvsuclem2  35554  satf0  35566  dfon2lem5  35979  seglelin  36310  bj-prmoore  37320  wl-ifp4impr  37672  wl-df4-3mintru2  37692  poimirlem30  37851  poimirlem31  37852  cnambfre  37869  fimgmcyclem  42788  expdioph  43265  dflim5  43571  rp-isfinite6  43759  uneqsn  44266
  Copyright terms: Public domain W3C validator