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

Theorem andi 857
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 385 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
2 olc 384 . . 3  |-  ( (
ph  /\  ch )  ->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
31, 2jaodan 778 . 2  |-  ( (
ph  /\  ( ps  \/  ch ) )  -> 
( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
4 orc 385 . . . 4  |-  ( ps 
->  ( ps  \/  ch ) )
54anim2i 566 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ( ps  \/  ch ) ) )
6 olc 384 . . . 4  |-  ( ch 
->  ( ps  \/  ch ) )
76anim2i 566 . . 3  |-  ( (
ph  /\  ch )  ->  ( ph  /\  ( ps  \/  ch ) ) )
85, 7jaoi 379 . 2  |-  ( ( ( ph  /\  ps )  \/  ( ph  /\ 
ch ) )  -> 
( ph  /\  ( ps  \/  ch ) ) )
93, 8impbii 188 1  |-  ( (
ph  /\  ( ps  \/  ch ) )  <->  ( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 368    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371
This theorem is referenced by:  andir  858  anddi  860  cadan  1438  thema1a  1584  indi  3593  indifdir  3603  unrab  3618  unipr  4101  uniun  4107  unopab  4364  ordnbtwn  4805  xpundi  4887  difxp  5259  coundir  5337  imadif  5490  unpreima  5826  tpostpos  6764  elznn0nn  10656  faclbnd4lem4  12068  opsrtoslem1  17541  mbfmax  21086  fta1glem2  21597  ofmulrt  21707  lgsquadlem3  22654  ordtconlem1  26290  ballotlemodife  26810  subfacp1lem6  27003  soseq  27644  nobnddown  27771  lineunray  28107  itg2addnclem2  28369  lzunuz  29031  diophun  29037  rmydioph  29288
  Copyright terms: Public domain W3C validator