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

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

Proof of Theorem andir
StepHypRef Expression
1 andi 910 . 2 ((𝜒 ∧ (𝜑𝜓)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
2 ancom 466 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑𝜓)))
3 ancom 466 . . 3 ((𝜑𝜒) ↔ (𝜒𝜑))
4 ancom 466 . . 3 ((𝜓𝜒) ↔ (𝜒𝜓))
53, 4orbi12i 543 . 2 (((𝜑𝜒) ∨ (𝜓𝜒)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
61, 2, 53bitr4i 292 1 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∨ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 383  wa 384
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 385  df-an 386
This theorem is referenced by:  anddi  913  cases  991  cador  1544  rexun  3776  rabun2  3887  reuun2  3891  xpundir  5138  coundi  5600  mptun  5987  tpostpos  7324  wemapsolem  8407  ltxr  11901  hashbclem  13182  hashf1lem2  13186  pythagtriplem2  15457  pythagtrip  15474  vdwapun  15613  legtrid  25403  colinearalg  25707  vtxdun  26280  elimifd  29232  dfon2lem5  31428  nobndup  31598  seglelin  31900  poimirlem30  33106  poimirlem31  33107  cnambfre  33125  expdioph  37105  rp-isfinite6  37380  uneqsn  37838
  Copyright terms: Public domain W3C validator