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  3322  indifdir  3332  unrab  3346  unipr  3741  uniun  3746  unopab  3992  trsuc2OLD  4370  ordnbtwn  4376  xpundi  4648  coundir  5081  imadif  5184  unpreima  5503  difxp  6005  tpostpos  6106  elznn0nn  9916  faclbnd4lem4  11187  opsrtoslem1  16057  mbfmax  18836  fta1glem2  19384  ofmulrt  19494  lgsquadlem3  20427  subfacp1lem6  22887  soseq  23422  axfelem10  23523  lineunray  23944  anddi2  24106  condisd  24108  lzunuz  26013  diophun  26019  rmydioph  26273
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