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

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

Proof of Theorem andir
StepHypRef Expression
1 andi 947 . 2 ((𝜒 ∧ (𝜑𝜓)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
2 ancom 465 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑𝜓)))
3 ancom 465 . . 3 ((𝜑𝜒) ↔ (𝜒𝜑))
4 ancom 465 . . 3 ((𝜓𝜒) ↔ (𝜒𝜓))
53, 4orbi12i 544 . 2 (((𝜑𝜒) ∨ (𝜓𝜒)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
61, 2, 53bitr4i 292 1 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∨ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  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 197  df-or 384  df-an 385
This theorem is referenced by:  anddi  950  cases  1029  cador  1696  rexun  3936  rabun2  4049  reuun2  4053  xpundir  5329  coundi  5797  mptun  6186  tpostpos  7541  wemapsolem  8620  ltxr  12142  hashbclem  13428  hashf1lem2  13432  pythagtriplem2  15724  pythagtrip  15741  vdwapun  15880  legtrid  25685  colinearalg  25989  vtxdun  26587  elimifd  29669  dfon2lem5  31997  seglelin  32529  poimirlem30  33752  poimirlem31  33753  cnambfre  33771  expdioph  38092  rp-isfinite6  38366  uneqsn  38823
  Copyright terms: Public domain W3C validator