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

Theorem andi 838
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 375 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
2 olc 374 . . 3  |-  ( (
ph  /\  ch )  ->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
31, 2jaodan 761 . 2  |-  ( (
ph  /\  ( ps  \/  ch ) )  -> 
( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
4 orc 375 . . . 4  |-  ( ps 
->  ( ps  \/  ch ) )
54anim2i 553 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ( ps  \/  ch ) ) )
6 olc 374 . . . 4  |-  ( ch 
->  ( ps  \/  ch ) )
76anim2i 553 . . 3  |-  ( (
ph  /\  ch )  ->  ( ph  /\  ( ps  \/  ch ) ) )
85, 7jaoi 369 . 2  |-  ( ( ( ph  /\  ps )  \/  ( ph  /\ 
ch ) )  -> 
( ph  /\  ( ps  \/  ch ) ) )
93, 8impbii 181 1  |-  ( (
ph  /\  ( ps  \/  ch ) )  <->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    \/ wo 358    /\ wa 359
This theorem is referenced by:  andir  839  anddi  841  indi  3547  indifdir  3557  unrab  3572  unipr  3989  uniun  3994  unopab  4244  ordnbtwn  4631  xpundi  4889  coundir  5331  imadif  5487  unpreima  5815  difxp  6339  tpostpos  6458  elznn0nn  10251  faclbnd4lem4  11542  opsrtoslem1  16499  mbfmax  19494  fta1glem2  20042  ofmulrt  20152  lgsquadlem3  21093  ballotlemodife  24708  subfacp1lem6  24824  soseq  25468  lineunray  25985  itg2addnclem2  26156  lzunuz  26716  diophun  26722  rmydioph  26975
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 178  df-or 360  df-an 361
  Copyright terms: Public domain W3C validator