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

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

Proof of Theorem andir
StepHypRef Expression
1 andi 907 . 2 ((𝜒 ∧ (𝜑𝜓)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
2 ancom 465 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑𝜓)))
3 ancom 465 . . 3 ((𝜑𝜒) ↔ (𝜒𝜑))
4 ancom 465 . . 3 ((𝜓𝜒) ↔ (𝜒𝜓))
53, 4orbi12i 542 . 2 (((𝜑𝜒) ∨ (𝜓𝜒)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
61, 2, 53bitr4i 291 1 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∨ (𝜓𝜒)))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∨ wo 382   ∧ wa 383 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 196  df-or 384  df-an 385 This theorem is referenced by:  anddi  910  cases  1004  cador  1538  rexun  3755  rabun2  3865  reuun2  3869  xpundir  5095  coundi  5553  mptun  5938  tpostpos  7259  wemapsolem  8338  ltxr  11825  hashbclem  13093  hashf1lem2  13097  pythagtriplem2  15360  pythagtrip  15377  vdwapun  15516  legtrid  25286  colinearalg  25590  usgraedg4  25916  vdgrun  26428  vdgrfiun  26429  elimifd  28746  dfon2lem5  30936  nobndup  31099  nofulllem5  31105  seglelin  31393  poimirlem30  32609  poimirlem31  32610  cnambfre  32628  expdioph  36608  rp-isfinite6  36883  uneqsn  37341  vtxdun  40696
 Copyright terms: Public domain W3C validator