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  3415  indifdir  3425  unrab  3439  unipr  3841  uniun  3846  unopab  4095  trsuc2OLD  4477  ordnbtwn  4483  xpundi  4741  coundir  5175  imadif  5327  unpreima  5651  difxp  6153  tpostpos  6254  elznn0nn  10037  faclbnd4lem4  11309  opsrtoslem1  16225  mbfmax  19004  fta1glem2  19552  ofmulrt  19662  lgsquadlem3  20595  ballotlemodife  23056  subfacp1lem6  23716  soseq  24254  nobnddown  24355  lineunray  24770  anddi2  24941  condisd  24943  lzunuz  26847  diophun  26853  rmydioph  27107
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