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

Theorem andi 867
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 385 . . 3
2 olc 384 . . 3
31, 2jaodan 785 . 2
4 orc 385 . . . 4
54anim2i 569 . . 3
6 olc 384 . . . 4
76anim2i 569 . . 3
85, 7jaoi 379 . 2
93, 8impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  \/wo 368  /\wa 369
This theorem is referenced by:  andir  868  anddi  870  cadan  1459  stoic1a  1605  indi  3743  indifdir  3753  unrab  3768  unipr  4262  uniun  4268  unopab  4527  ordnbtwn  4973  xpundi  5057  difxp  5436  coundir  5514  imadif  5668  unpreima  6013  tpostpos  6994  elznn0nn  10903  faclbnd4lem4  12374  opsrtoslem1  18148  mbfmax  22056  fta1glem2  22567  ofmulrt  22678  lgsquadlem3  23631  ordtconlem1  27906  ballotlemodife  28436  subfacp1lem6  28629  soseq  29334  nobnddown  29461  lineunray  29797  itg2addnclem2  30067  lzunuz  30701  diophun  30707  rmydioph  30956  rp-isfinite6  37744
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 185  df-or 370  df-an 371
  Copyright terms: Public domain W3C validator