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

Theorem 3eqtr3rd 2324
Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)
Hypotheses
Ref Expression
3eqtr3d.1  |-  ( ph  ->  A  =  B )
3eqtr3d.2  |-  ( ph  ->  A  =  C )
3eqtr3d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3eqtr3rd  |-  ( ph  ->  D  =  C )

Proof of Theorem 3eqtr3rd
StepHypRef Expression
1 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
2 3eqtr3d.1 . . 3  |-  ( ph  ->  A  =  B )
3 3eqtr3d.2 . . 3  |-  ( ph  ->  A  =  C )
42, 3eqtr3d 2317 . 2  |-  ( ph  ->  B  =  C )
51, 4eqtr3d 2317 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  fcofo  5798  fcof1o  5803  cantnfp1lem3  7382  fin1a2lem7  8032  prlem934  8657  addid2  8995  addcom  8998  addcomd  9014  negeu  9042  add20  9286  2halves  9940  bcnn  11324  bcpasc  11333  hashfun  11389  wrdeqs1cat  11475  sqreulem  11843  summolem3  12187  fsumneg  12249  geolim  12326  geolim2  12327  mertens  12342  sincossq  12456  demoivre  12480  eirrlem  12482  sadeq  12663  gcdid  12710  phiprmpw  12844  pythagtriplem12  12879  expnprm  12950  fullresc  13725  grpinvid1  14530  grpnpcan  14557  grplactcnv  14564  conjghm  14713  odmodnn0  14855  gex1  14902  sylow3lem3  14940  efgredeu  15061  odadd2  15141  gsumval3  15191  pgpfac1lem3a  15311  rngnegl  15380  rngnegr  15381  rngmneg2  15383  lmodvsneg  15669  lss0v  15773  lssvs0or  15863  lvecinv  15866  lspabs2  15873  mplcoe3  16210  mplcoe2  16211  zrngunit  16438  zcyg  16445  paste  17022  ngpds  18125  ioo2bl  18299  ipcau2  18664  dvexp3  19325  rolle  19337  cmvth  19338  dv11cn  19348  lhop  19363  itgsubstlem  19395  ply1divex  19522  fta1glem1  19551  fta1g  19553  fta1  19688  vieta1lem2  19691  aaliou2  19720  dvtaylp  19749  dvntaylp  19750  taylthlem1  19752  taylthlem2  19753  dvradcnv  19797  ptolemy  19864  coskpi  19888  tanregt0  19901  cxpeq  20097  isosctrlem2  20119  chordthmlem  20129  dcubic  20142  quart1lem  20151  tanatan  20215  atantan  20219  dvatan  20231  birthdaylem2  20247  rlimcxp  20268  jensenlem2  20282  emcllem2  20290  basellem8  20325  bclbnd  20519  lgsqr  20585  lgseisenlem3  20590  lgseisenlem4  20591  lgsquadlem1  20593  lgsquadlem2  20594  rpvmasumlem  20636  dchrisumlem1  20638  dchrisum0flblem1  20657  dchrisum0flblem2  20658  dchrisum0re  20662  dchrisum0lem1  20665  mudivsum  20679  mulogsum  20681  vmalogdivsum2  20687  logsqvma2  20692  selberg2lem  20699  logdivbnd  20705  selbergr  20717  selberg3r  20718  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntpbnd2  20736  grpoinvid1  20897  vcz  21126  hosubsub4  22398  lnop0  22546  branmfn  22685  ballotlemfrceq  23087  ballotlemrinv0  23091  brbtwn2  24533  colinearalglem4  24537  axsegconlem9  24553  ax5seglem1  24556  axbtwnid  24567  axeuclidlem  24590  axcontlem2  24593  axcontlem4  24595  bpoly3  24793  dvreasin  24923  areacirclem2  24925  areacirclem5  24929  fprodsub  25379  cnegvex2  25660  rngonegmn1l  26580  rngonegmn1r  26581  irrapxlem5  26911  pellfund14  26983  rmxdbl  27024  jm2.22  27088  dgrnznn  27340  sigariz  27853  lfl0  29255  latmassOLD  29419  omlmod1i2N  29450  llnexchb2lem  30057  dalawlem3  30062  pmapj2N  30118  osumcllem9N  30153  pexmidlem6N  30164  4atexlemc  30258  cdleme1  30416  cdleme42a  30660  cdlemg13a  30840  cdlemh2  31005  cdlemk1  31020  tendocnv  31211  dihmeetlem12N  31508  dihmeetlem16N  31512  dihmeetlem19N  31515  dochsatshp  31641  dochexmidlem6  31655  mapdval4N  31822  mapdpglem28  31891  mapdpglem31  31893  mapdindp4  31913  hdmap14lem1a  32059  hdmapinvlem4  32114
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator