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

Theorem andi 837
Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
Assertion
Ref Expression
andi  |-  ( (
ph  /\  ( ps  \/  ch ) )  <->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )

Proof of Theorem andi
StepHypRef Expression
1 orc 374 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
2 olc 373 . . 3  |-  ( (
ph  /\  ch )  ->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
31, 2jaodan 760 . 2  |-  ( (
ph  /\  ( ps  \/  ch ) )  -> 
( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
4 orc 374 . . . 4  |-  ( ps 
->  ( ps  \/  ch ) )
54anim2i 552 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ( ps  \/  ch ) ) )
6 olc 373 . . . 4  |-  ( ch 
->  ( ps  \/  ch ) )
76anim2i 552 . . 3  |-  ( (
ph  /\  ch )  ->  ( ph  /\  ( ps  \/  ch ) ) )
85, 7jaoi 368 . 2  |-  ( ( ( ph  /\  ps )  \/  ( ph  /\ 
ch ) )  -> 
( ph  /\  ( ps  \/  ch ) ) )
93, 8impbii 180 1  |-  ( (
ph  /\  ( ps  \/  ch ) )  <->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357    /\ wa 358
This theorem is referenced by:  andir  838  anddi  840  indi  3428  indifdir  3438  unrab  3452  unipr  3857  uniun  3862  unopab  4111  trsuc2OLD  4493  ordnbtwn  4499  xpundi  4757  coundir  5191  imadif  5343  unpreima  5667  difxp  6169  tpostpos  6270  elznn0nn  10053  faclbnd4lem4  11325  opsrtoslem1  16241  mbfmax  19020  fta1glem2  19568  ofmulrt  19678  lgsquadlem3  20611  ballotlemodife  23072  subfacp1lem6  23731  soseq  24325  nobnddown  24426  lineunray  24842  itg2addnclem2  25004  anddi2  25044  condisd  25046  lzunuz  26950  diophun  26956  rmydioph  27210
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360
  Copyright terms: Public domain W3C validator