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

Theorem andi 907
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 399 . . 3 ((𝜑𝜓) → ((𝜑𝜓) ∨ (𝜑𝜒)))
2 olc 398 . . 3 ((𝜑𝜒) → ((𝜑𝜓) ∨ (𝜑𝜒)))
31, 2jaodan 822 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (𝜑𝜒)))
4 orc 399 . . . 4 (𝜓 → (𝜓𝜒))
54anim2i 591 . . 3 ((𝜑𝜓) → (𝜑 ∧ (𝜓𝜒)))
6 olc 398 . . . 4 (𝜒 → (𝜓𝜒))
76anim2i 591 . . 3 ((𝜑𝜒) → (𝜑 ∧ (𝜓𝜒)))
85, 7jaoi 393 . 2 (((𝜑𝜓) ∨ (𝜑𝜒)) → (𝜑 ∧ (𝜓𝜒)))
93, 8impbii 198 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:  andir  908  anddi  910  cadan  1539  indi  3832  indifdir  3842  unrab  3857  unipr  4385  uniun  4392  unopab  4660  xpundi  5094  difxp  5477  coundir  5554  ordnbtwnOLD  5734  imadif  5887  unpreima  6249  tpostpos  7259  elznn0nn  11268  faclbnd4lem4  12945  opsrtoslem1  19305  mbfmax  23222  fta1glem2  23730  ofmulrt  23841  lgsquadlem3  24907  ordtconlem1  29298  ballotlemodife  29886  subfacp1lem6  30421  soseq  30995  nobnddown  31100  lineunray  31424  poimirlem30  32609  itg2addnclem2  32632  lzunuz  36349  diophun  36355  rmydioph  36599  rp-isfinite6  36883  relexpxpmin  37028  andi3or  37340  clsk1indlem3  37361  zeoALTV  40119
  Copyright terms: Public domain W3C validator