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

Theorem andi 1035
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 898 . . 3 ((𝜑𝜓) → ((𝜑𝜓) ∨ (𝜑𝜒)))
2 olc 899 . . 3 ((𝜑𝜒) → ((𝜑𝜓) ∨ (𝜑𝜒)))
31, 2jaodan 985 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (𝜑𝜒)))
4 orc 898 . . . 4 (𝜓 → (𝜓𝜒))
54anim2i 610 . . 3 ((𝜑𝜓) → (𝜑 ∧ (𝜓𝜒)))
6 olc 899 . . . 4 (𝜒 → (𝜓𝜒))
76anim2i 610 . . 3 ((𝜑𝜒) → (𝜑 ∧ (𝜓𝜒)))
85, 7jaoi 888 . 2 (((𝜑𝜓) ∨ (𝜑𝜒)) → (𝜑 ∧ (𝜓𝜒)))
93, 8impbii 201 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 386  wo 878
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 199  df-an 387  df-or 879
This theorem is referenced by:  andir  1036  anddi  1038  annotanannotOLD  1039  cadan  1722  indi  4103  indifdir  4113  unrab  4127  unipr  4671  uniun  4679  unopab  4951  xpundi  5404  difxp  5799  coundir  5878  imadif  6206  unpreima  6590  tpostpos  7637  elznn0nn  11718  faclbnd4lem4  13376  opsrtoslem1  19844  mbfmax  23815  fta1glem2  24325  ofmulrt  24436  lgsquadlem3  25520  difrab2  29876  ordtconnlem1  30504  ballotlemodife  31094  subfacp1lem6  31702  soseq  32282  nosep1o  32360  lineunray  32782  bj-ismooredr2  33581  poimirlem30  33976  itg2addnclem2  33998  lzunuz  38168  diophun  38174  rmydioph  38417  rp-isfinite6  38698  relexpxpmin  38843  andi3or  39153  clsk1indlem3  39174  zeoALTV  42404
  Copyright terms: Public domain W3C validator