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

Theorem andi 839
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 376 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
2 olc 375 . . 3  |-  ( (
ph  /\  ch )  ->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
31, 2jaodan 762 . 2  |-  ( (
ph  /\  ( ps  \/  ch ) )  -> 
( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
4 orc 376 . . . 4  |-  ( ps 
->  ( ps  \/  ch ) )
54anim2i 554 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ( ps  \/  ch ) ) )
6 olc 375 . . . 4  |-  ( ch 
->  ( ps  \/  ch ) )
76anim2i 554 . . 3  |-  ( (
ph  /\  ch )  ->  ( ph  /\  ( ps  \/  ch ) ) )
85, 7jaoi 370 . 2  |-  ( ( ( ph  /\  ps )  \/  ( ph  /\ 
ch ) )  -> 
( ph  /\  ( ps  \/  ch ) ) )
93, 8impbii 182 1  |-  ( (
ph  /\  ( ps  \/  ch ) )  <->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    \/ wo 359    /\ wa 360
This theorem is referenced by:  andir  840  anddi  842  indi  3417  indifdir  3427  unrab  3441  unipr  3843  uniun  3848  unopab  4097  trsuc2OLD  4477  ordnbtwn  4483  xpundi  4741  coundir  5174  imadif  5293  unpreima  5613  difxp  6115  tpostpos  6216  elznn0nn  10033  faclbnd4lem4  11304  opsrtoslem1  16220  mbfmax  18999  fta1glem2  19547  ofmulrt  19657  lgsquadlem3  20590  ballotlemodife  23050  subfacp1lem6  23121  soseq  23656  axfelem10  23757  lineunray  24178  anddi2  24340  condisd  24342  lzunuz  26247  diophun  26253  rmydioph  26507
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362
  Copyright terms: Public domain W3C validator