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

Theorem andi 910
 Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
Assertion
Ref Expression
andi ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (𝜑𝜒)))

Proof of Theorem andi
StepHypRef Expression
1 orc 400 . . 3 ((𝜑𝜓) → ((𝜑𝜓) ∨ (𝜑𝜒)))
2 olc 399 . . 3 ((𝜑𝜒) → ((𝜑𝜓) ∨ (𝜑𝜒)))
31, 2jaodan 825 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (𝜑𝜒)))
4 orc 400 . . . 4 (𝜓 → (𝜓𝜒))
54anim2i 592 . . 3 ((𝜑𝜓) → (𝜑 ∧ (𝜓𝜒)))
6 olc 399 . . . 4 (𝜒 → (𝜓𝜒))
76anim2i 592 . . 3 ((𝜑𝜒) → (𝜑 ∧ (𝜓𝜒)))
85, 7jaoi 394 . 2 (((𝜑𝜓) ∨ (𝜑𝜒)) → (𝜑 ∧ (𝜓𝜒)))
93, 8impbii 199 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:  andir  911  anddi  913  cadan  1545  indi  3849  indifdir  3859  unrab  3874  unipr  4415  uniun  4422  unopab  4690  xpundi  5132  difxp  5517  coundir  5596  ordnbtwnOLD  5776  imadif  5931  unpreima  6297  tpostpos  7317  elznn0nn  11335  faclbnd4lem4  13023  opsrtoslem1  19403  mbfmax  23322  fta1glem2  23830  ofmulrt  23941  lgsquadlem3  25007  ordtconnlem1  29752  ballotlemodife  30340  subfacp1lem6  30875  soseq  31452  nobnddown  31564  lineunray  31896  poimirlem30  33071  itg2addnclem2  33094  lzunuz  36811  diophun  36817  rmydioph  37061  rp-isfinite6  37345  relexpxpmin  37490  andi3or  37802  clsk1indlem3  37823  zeoALTV  40880
 Copyright terms: Public domain W3C validator