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

Theorem andi 865
Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-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 783 . 2  |-  ( (
ph  /\  ( ps  \/  ch ) )  -> 
( ( ph  /\  ps )  \/  ( ph  /\  ch ) ) )
4 orc 385 . . . 4  |-  ( ps 
->  ( ps  \/  ch ) )
54anim2i 569 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ( ps  \/  ch ) ) )
6 olc 384 . . . 4  |-  ( ch 
->  ( ps  \/  ch ) )
76anim2i 569 . . 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  866  anddi  868  cadan  1443  thema1a  1589  indi  3749  indifdir  3759  unrab  3774  unipr  4264  uniun  4270  unopab  4528  ordnbtwn  4974  xpundi  5058  difxp  5437  coundir  5515  imadif  5669  unpreima  6014  tpostpos  6987  elznn0nn  10890  faclbnd4lem4  12354  opsrtoslem1  18018  mbfmax  21924  fta1glem2  22435  ofmulrt  22545  lgsquadlem3  23497  ordtconlem1  27731  ballotlemodife  28261  subfacp1lem6  28454  soseq  29261  nobnddown  29388  lineunray  29724  itg2addnclem2  29994  lzunuz  30629  diophun  30635  rmydioph  30884
  Copyright terms: Public domain W3C validator