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

Theorem andi 842
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 763 . 2  |-  ( (
ph  /\  ( ps  \/  ch ) )  -> 
( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
4 orc 376 . . . 4  |-  ( ps 
->  ( ps  \/  ch ) )
54anim2i 555 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ( ps  \/  ch ) ) )
6 olc 375 . . . 4  |-  ( ch 
->  ( ps  \/  ch ) )
76anim2i 555 . . 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  843  anddi  845  indi  3390  indifdir  3400  unrab  3414  unipr  3815  uniun  3820  unopab  4069  trsuc2OLD  4449  ordnbtwn  4455  xpundi  4729  coundir  5162  imadif  5265  unpreima  5585  difxp  6087  tpostpos  6188  elznn0nn  10004  faclbnd4lem4  11275  opsrtoslem1  16187  mbfmax  18966  fta1glem2  19514  ofmulrt  19624  lgsquadlem3  20557  ballotlemodife  23017  subfacp1lem6  23088  soseq  23623  axfelem10  23724  lineunray  24145  anddi2  24307  condisd  24309  lzunuz  26214  diophun  26220  rmydioph  26474
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