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

Theorem 3eqtr3rd 2504
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 2497 . 2  |-  ( ph  ->  B  =  C )
51, 4eqtr3d 2497 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446
This theorem is referenced by:  fcofo  6166  fcof1oinvd  6171  cantnfp1lem3  8090  cantnfp1lem3OLD  8116  fin1a2lem7  8777  prlem934  9400  addid2  9752  addcom  9755  addcomd  9771  negeu  9801  add20  10060  2halves  10763  bcnn  12372  bcpasc  12381  hashfun  12479  wrdeqs1cat  12691  sqreulem  13274  summolem3  13618  fsumneg  13684  geolim  13761  geolim2  13762  mertens  13777  prodmolem3  13822  sincossq  13993  demoivre  14017  eirrlem  14019  sadeq  14206  gcdid  14253  phiprmpw  14390  pythagtriplem12  14434  expnprm  14505  fullresc  15339  grpinvid1  16297  grpnpcan  16329  grplactcnv  16337  ghmgrp  16393  conjghm  16496  odmodnn0  16763  gex1  16810  sylow3lem3  16848  efgredeu  16969  odadd2  17054  gsumval3OLD  17107  gsumval3  17110  pgpfac1lem3a  17322  ringnegl  17435  rngnegr  17436  ringmneg2  17438  lmodvsneg  17749  lss0v  17857  lssvs0or  17951  lvecinv  17954  lspabs2  17961  mplcoe3  18323  mplcoe3OLD  18324  mplcoe5  18326  mplcoe2OLD  18328  evlvar  18393  zringcyg  18701  zringunit  18703  mdetrlin  19271  mdetunilem6  19286  cramerimplem3  19354  cramerimp  19355  paste  19962  tuslem  20936  tususs  20939  ngpds  21289  ioo2bl  21464  ipcau2  21843  dvexp3  22545  rolle  22557  cmvth  22558  dv11cn  22568  lhop  22583  itgsubstlem  22615  ply1divex  22703  fta1glem1  22732  fta1g  22734  dgrnznn  22810  fta1  22870  vieta1lem2  22873  aaliou2  22902  dvtaylp  22931  dvntaylp  22932  taylthlem1  22934  taylthlem2  22935  dvradcnv  22982  ptolemy  23055  coskpi  23079  tanregt0  23092  cxpeq  23299  isosctrlem2  23350  chordthmlem  23360  dcubic  23374  quart1lem  23383  tanatan  23447  atantan  23451  dvatan  23463  birthdaylem2  23480  rlimcxp  23501  jensenlem2  23515  logdiflbnd  23522  emcllem2  23524  basellem8  23559  bclbnd  23753  lgsqr  23819  lgseisenlem3  23824  lgseisenlem4  23825  lgsquadlem1  23827  lgsquadlem2  23828  rpvmasumlem  23870  dchrisumlem1  23872  dchrisum0flblem1  23891  dchrisum0flblem2  23892  dchrisum0re  23896  dchrisum0lem1  23899  mudivsum  23913  mulogsum  23915  vmalogdivsum2  23921  logsqvma2  23926  selberg2lem  23933  logdivbnd  23939  selbergr  23951  selberg3r  23952  pntrlog2bndlem4  23963  pntrlog2bndlem5  23964  pntpbnd2  23970  miduniq  24263  krippenlem  24268  colperpexlem2  24306  ttgcontlem1  24390  brbtwn2  24410  colinearalglem4  24414  axsegconlem9  24430  ax5seglem1  24433  axbtwnid  24444  axeuclidlem  24467  axcontlem2  24470  axcontlem4  24472  clwwlkel  24995  grpoinvid1  25430  vcz  25661  hosubsub4  26935  lnop0  27083  branmfn  27222  iunxdif3  27637  difico  27828  omndmul2  27936  rdivmuldivd  28016  kerunit  28048  carsggect  28526  carsgclctunlem2  28527  ballotlemfrceq  28731  ballotlemrinv0  28735  wrdsplex  28759  lgamgulmlem2  28836  lgamcvg2  28861  fallrisefac  29388  faclimlem1  29409  bpoly3  30048  mblfinlem2  30292  voliunnfl  30298  volsupnfl  30299  itg2addnclem3  30308  ftc2nc  30339  dvasin  30343  areacirclem1  30347  areacirclem4  30350  rngonegmn1l  30592  rngonegmn1r  30593  irrapxlem5  31001  pellfund14  31073  rmxdbl  31114  jm2.22  31176  itgpowd  31423  0ellimcdiv  31894  fourierdlem95  32223  etransclem46  32302  sigariz  32319  altgsumbc  33195  blengt1fldiv2p1  33468  lfl0  35187  latmassOLD  35351  omlmod1i2N  35382  llnexchb2lem  35989  dalawlem3  35994  pmapj2N  36050  osumcllem9N  36085  pexmidlem6N  36096  4atexlemc  36190  cdleme1  36349  cdleme42a  36594  cdlemg13a  36774  cdlemh2  36939  cdlemk1  36954  tendocnv  37145  dihmeetlem12N  37442  dihmeetlem16N  37446  dihmeetlem19N  37449  dochsatshp  37575  dochexmidlem6  37589  mapdval4N  37756  mapdpglem28  37825  mapdpglem31  37827  mapdindp4  37847  hdmap14lem1a  37993  hdmapinvlem4  38048
  Copyright terms: Public domain W3C validator