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

Theorem andi 1005
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 865 . . 3 ((𝜑𝜓) → ((𝜑𝜓) ∨ (𝜑𝜒)))
2 olc 866 . . 3 ((𝜑𝜒) → ((𝜑𝜓) ∨ (𝜑𝜒)))
31, 2jaodan 955 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (𝜑𝜒)))
4 orc 865 . . . 4 (𝜓 → (𝜓𝜒))
54anim2i 615 . . 3 ((𝜑𝜓) → (𝜑 ∧ (𝜓𝜒)))
6 olc 866 . . . 4 (𝜒 → (𝜓𝜒))
76anim2i 615 . . 3 ((𝜑𝜒) → (𝜑 ∧ (𝜓𝜒)))
85, 7jaoi 855 . 2 (((𝜑𝜓) ∨ (𝜑𝜒)) → (𝜑 ∧ (𝜓𝜒)))
93, 8impbii 208 1 ((𝜑 ∧ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  wo 845
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 206  df-an 395  df-or 846
This theorem is referenced by:  andir  1006  anddi  1008  cadan  1602  indi  4272  indifdirOLD  4284  unrab  4304  uniprOLD  4927  uniun  4934  unopab  5231  xpundi  5746  difxp  6170  coundir  6254  imadif  6638  unpreima  7071  soseq  8164  tpostpos  8252  elznn0nn  12605  faclbnd4lem4  14291  opsrtoslem1  22021  mbfmax  25622  fta1glem2  26148  ofmulrt  26261  lgsquadlem3  27360  nogesgn1o  27652  nosep1o  27660  noinfbnd2lem1  27709  difrab2  32374  ordtconnlem1  33656  ballotlemodife  34248  subfacp1lem6  34926  satf0op  35118  lineunray  35874  wl-ifpimpr  37076  wl-df2-3mintru2  37095  poimirlem30  37254  itg2addnclem2  37276  sticksstones22  41771  lzunuz  42330  diophun  42335  rmydioph  42577  fzunt  43027  fzuntd  43028  fzunt1d  43029  fzuntgd  43030  rp-isfinite6  43090  relexpxpmin  43289  andi3or  43596  clsk1indlem3  43615  simpcntrab  46396  zeoALTV  47147
  Copyright terms: Public domain W3C validator