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

Theorem 3eqtr3rd 2430
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 2423 . 2  |-  ( ph  ->  B  =  C )
51, 4eqtr3d 2423 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  fcofo  5962  fcof1o  5967  cantnfp1lem3  7571  fin1a2lem7  8221  prlem934  8845  addid2  9183  addcom  9186  addcomd  9202  negeu  9230  add20  9474  2halves  10130  bcnn  11532  bcpasc  11541  hashfun  11629  wrdeqs1cat  11718  sqreulem  12092  summolem3  12437  fsumneg  12499  geolim  12576  geolim2  12577  mertens  12592  sincossq  12706  demoivre  12730  eirrlem  12732  sadeq  12913  gcdid  12960  phiprmpw  13094  pythagtriplem12  13129  expnprm  13200  fullresc  13977  grpinvid1  14782  grpnpcan  14809  grplactcnv  14816  conjghm  14965  odmodnn0  15107  gex1  15154  sylow3lem3  15192  efgredeu  15313  odadd2  15393  gsumval3  15443  pgpfac1lem3a  15563  rngnegl  15632  rngnegr  15633  rngmneg2  15635  lmodvsneg  15917  lss0v  16021  lssvs0or  16111  lvecinv  16114  lspabs2  16121  mplcoe3  16458  mplcoe2  16459  zrngunit  16690  zcyg  16697  paste  17282  tuslem  18220  tususs  18223  ngpds  18523  ioo2bl  18697  ipcau2  19064  dvexp3  19731  rolle  19743  cmvth  19744  dv11cn  19754  lhop  19769  itgsubstlem  19801  ply1divex  19928  fta1glem1  19957  fta1g  19959  fta1  20094  vieta1lem2  20097  aaliou2  20126  dvtaylp  20155  dvntaylp  20156  taylthlem1  20158  taylthlem2  20159  dvradcnv  20206  ptolemy  20273  coskpi  20297  tanregt0  20310  cxpeq  20510  isosctrlem2  20532  chordthmlem  20542  dcubic  20555  quart1lem  20564  tanatan  20628  atantan  20632  dvatan  20644  birthdaylem2  20660  rlimcxp  20681  jensenlem2  20695  logdiflbnd  20702  emcllem2  20704  basellem8  20739  bclbnd  20933  lgsqr  20999  lgseisenlem3  21004  lgseisenlem4  21005  lgsquadlem1  21007  lgsquadlem2  21008  rpvmasumlem  21050  dchrisumlem1  21052  dchrisum0flblem1  21071  dchrisum0flblem2  21072  dchrisum0re  21076  dchrisum0lem1  21079  mudivsum  21093  mulogsum  21095  vmalogdivsum2  21101  logsqvma2  21106  selberg2lem  21113  logdivbnd  21119  selbergr  21131  selberg3r  21132  pntrlog2bndlem4  21143  pntrlog2bndlem5  21144  pntpbnd2  21150  grpoinvid1  21668  vcz  21899  hosubsub4  23171  lnop0  23319  branmfn  23458  difico  23984  rdivmuldivd  24058  kerunit  24079  ballotlemfrceq  24567  ballotlemrinv0  24571  lgamgulmlem2  24595  lgamcvg2  24620  prodmolem3  25040  fallrisefac  25111  faclimlem1  25122  brbtwn2  25560  colinearalglem4  25564  axsegconlem9  25580  ax5seglem1  25583  axbtwnid  25594  axeuclidlem  25617  axcontlem2  25620  axcontlem4  25622  bpoly3  25820  voliunnfl  25957  volsupnfl  25958  dvreasin  25982  areacirclem2  25984  areacirclem5  25988  rngonegmn1l  26258  rngonegmn1r  26259  irrapxlem5  26582  pellfund14  26654  rmxdbl  26695  jm2.22  26759  dgrnznn  27011  sigariz  27523  lfl0  29182  latmassOLD  29346  omlmod1i2N  29377  llnexchb2lem  29984  dalawlem3  29989  pmapj2N  30045  osumcllem9N  30080  pexmidlem6N  30091  4atexlemc  30185  cdleme1  30343  cdleme42a  30587  cdlemg13a  30767  cdlemh2  30932  cdlemk1  30947  tendocnv  31138  dihmeetlem12N  31435  dihmeetlem16N  31439  dihmeetlem19N  31442  dochsatshp  31568  dochexmidlem6  31582  mapdval4N  31749  mapdpglem28  31818  mapdpglem31  31820  mapdindp4  31840  hdmap14lem1a  31986  hdmapinvlem4  32041
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2382
  Copyright terms: Public domain W3C validator