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

Theorem andi 1003
 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 863 . . 3 ((𝜑𝜓) → ((𝜑𝜓) ∨ (𝜑𝜒)))
2 olc 864 . . 3 ((𝜑𝜒) → ((𝜑𝜓) ∨ (𝜑𝜒)))
31, 2jaodan 953 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (𝜑𝜒)))
4 orc 863 . . . 4 (𝜓 → (𝜓𝜒))
54anim2i 618 . . 3 ((𝜑𝜓) → (𝜑 ∧ (𝜓𝜒)))
6 olc 864 . . . 4 (𝜒 → (𝜓𝜒))
76anim2i 618 . . 3 ((𝜑𝜒) → (𝜑 ∧ (𝜓𝜒)))
85, 7jaoi 853 . 2 (((𝜑𝜓) ∨ (𝜑𝜒)) → (𝜑 ∧ (𝜓𝜒)))
93, 8impbii 211 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (𝜑𝜒)))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208   ∧ wa 398   ∨ wo 843 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 209  df-an 399  df-or 844 This theorem is referenced by:  andir  1004  anddi  1006  cadan  1603  indi  4248  indifdir  4258  unrab  4272  unipr  4843  uniun  4849  unopab  5136  xpundi  5613  difxp  6014  coundir  6094  imadif  6431  unpreima  6826  tpostpos  7904  elznn0nn  11987  faclbnd4lem4  13648  opsrtoslem1  20256  mbfmax  24242  fta1glem2  24752  ofmulrt  24863  lgsquadlem3  25950  difrab2  30253  ordtconnlem1  31160  ballotlemodife  31748  subfacp1lem6  32425  satf0op  32617  soseq  33089  nosep1o  33179  lineunray  33601  poimirlem30  34914  itg2addnclem2  34936  lzunuz  39355  diophun  39360  rmydioph  39601  rp-isfinite6  39874  relexpxpmin  40052  andi3or  40362  clsk1indlem3  40383  simpcntrab  43117  zeoALTV  43825
 Copyright terms: Public domain W3C validator