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

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

Proof of Theorem andir
StepHypRef Expression
1 andi 973 . 2 ((𝜒 ∧ (𝜑𝜓)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
2 ancom 452 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜒 ∧ (𝜑𝜓)))
3 ancom 452 . . 3 ((𝜑𝜒) ↔ (𝜒𝜑))
4 ancom 452 . . 3 ((𝜓𝜒) ↔ (𝜒𝜓))
53, 4orbi12i 888 . 2 (((𝜑𝜒) ∨ (𝜓𝜒)) ↔ ((𝜒𝜑) ∨ (𝜒𝜓)))
61, 2, 53bitr4i 292 1 (((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∨ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382  wo 826
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-an 383  df-or 827
This theorem is referenced by:  anddi  976  cases  1028  cador  1695  rexun  3944  rabun2  4054  reuun2  4058  xpundir  5312  coundi  5780  mptun  6165  tpostpos  7524  wemapsolem  8611  ltxr  12154  hashbclem  13438  hashf1lem2  13442  pythagtriplem2  15729  pythagtrip  15746  vdwapun  15885  legtrid  25707  colinearalg  26011  vtxdun  26612  elimifd  29700  dfon2lem5  32028  seglelin  32560  poimirlem30  33772  poimirlem31  33773  cnambfre  33790  expdioph  38116  rp-isfinite6  38390  uneqsn  38847
  Copyright terms: Public domain W3C validator