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

Theorem 3eqtr4rd 2506
Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)
Hypotheses
Ref Expression
3eqtr4d.1  |-  ( ph  ->  A  =  B )
3eqtr4d.2  |-  ( ph  ->  C  =  A )
3eqtr4d.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3eqtr4rd  |-  ( ph  ->  D  =  C )

Proof of Theorem 3eqtr4rd
StepHypRef Expression
1 3eqtr4d.3 . . 3  |-  ( ph  ->  D  =  B )
2 3eqtr4d.1 . . 3  |-  ( ph  ->  A  =  B )
31, 2eqtr4d 2498 . 2  |-  ( ph  ->  D  =  A )
4 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
53, 4eqtr4d 2498 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446
This theorem is referenced by:  csbun  3818  csbcnvgALT  5133  csbres  5222  odi  7129  phplem4  7604  cantnfp1lem3  8000  cantnfp1  8001  cantnfp1lem3OLD  8026  cantnfp1OLD  8027  cardidm  8241  ackbij2lem2  8521  ackbij2lem3  8522  divneg  10138  xadddilem  11369  xadddi2  11372  dfceil2  11798  modlt  11836  modmulnn  11843  seqcaopr3  11959  bcval5  12212  hashgadd  12259  hashun3  12266  seqcoll  12335  swrdccatwrd  12481  cshwmodn  12551  2cshwcom  12569  revco  12581  cshco  12583  cjreb  12731  recj  12732  imcj  12740  imval2  12759  sqrmul  12868  absmax  12936  amgm2  12976  summolem2a  13311  fsumf1o  13319  sumsn  13336  sumsplit  13354  fsummulc2  13370  binom  13412  bcxmas  13417  incexclem  13418  incexc  13419  expcnv  13445  cvgrat  13462  ege2le3  13494  efaddlem  13497  eftlub  13512  tanval3  13537  tanneg  13551  cosmul  13576  cos01bnd  13589  demoivreALT  13604  absmulgcd  13850  eulerthlem2  13976  pythagtriplem14  14014  pcmul  14037  pcfac  14080  prmreclem6  14101  4sqlem12  14136  vdwlem6  14166  oppccatid  14778  curf2ndf  15177  oppcyon  15199  joincomALT  15319  meetcomALT  15321  pwsco1mhm  15618  mulgnn0p1  15758  mulgneg  15765  mulgnn0dir  15770  divsgrp2  15793  divsghm  15903  gaid  15937  pmtrdifellem3  16104  psgnunilem2  16121  odmulg  16179  sylow1lem2  16220  sylow2a  16240  sylow3lem1  16248  efgredleme  16362  efgcpbllemb  16374  gsumzaddlem  16530  gsumzaddlemOLD  16532  gsumconst  16550  gsumzmhm  16553  gsumzmhmOLD  16554  srgpcomp  16754  srgbinom  16767  lmodsubdi  17126  0lmhm  17245  lspsneq  17327  divsrhm  17443  divscrng  17446  asclrhm  17536  resspsrmul  17614  evlsscasrng  17737  psropprmul  17817  evls1scasrng  17899  zringlpirlem3  18031  zlpirlem3  18036  mulgrhm  18052  mulgrhmOLD  18055  frlmip  18329  frlmphl  18332  1marepvmarrepid  18514  mdetrlin  18541  mdetrsca2  18543  mdetunilem7  18557  mdetunilem9  18559  mndifsplit  18575  maducoeval2  18579  smadiadetglem2  18611  ptbasfi  19287  ptuni  19300  alexsubALTlem3  19754  subgtgp  19809  tsmsxplem1  19860  xmsuspOLD  20293  xmsusp  20294  restmetu  20295  nminv  20345  nrginvrcnlem  20404  copco  20723  pcoass  20729  pi1bas  20743  pi1xfrf  20758  pi1xfr  20760  cph2subdi  20861  cphassr  20863  tchcphlem1  20883  rrxip  21027  rrxnm  21028  pjthlem1  21057  ovolunlem1a  21112  ovolfs2  21185  uniiccdif  21192  ismbf  21242  itgaddlem2  21435  ditgswap  21468  ply1divex  21742  plyeq0lem  21812  plymullem1  21816  dgrcolem2  21875  vieta1lem2  21911  elqaalem2  21920  elqaalem3  21921  aaliou3lem7  21949  ulmshft  21989  mulcxplem  22263  cxpmul2  22268  root1eq1  22327  cxpeq  22329  cosangneg2d  22337  isosctrlem2  22351  angpieqvdlem  22357  chordthmlem3  22363  chordthmlem4  22364  chordthmlem5  22365  quad2  22368  dcubic2  22373  cubic2  22377  quart1  22385  scvxcvx  22513  basellem9  22560  ppifl  22632  mumul  22653  sgmmul  22674  chtublem  22684  chpub  22693  logfacrlim  22697  dchrsum2  22741  sumdchr2  22743  bposlem9  22765  lgsdir2  22801  lgsdir  22803  lgsdi  22805  lgsdirnn0  22812  lgsdinn0  22813  2sqblem  22850  chpo1ub  22863  dchrmusum2  22877  dchrvmasumlem1  22878  dchrvmasum2if  22880  dchrisum0fmul  22889  rpvmasum2  22895  mulog2sumlem1  22917  vmalogdivsum2  22921  log2sumbnd  22927  selberg3lem1  22940  selberg4lem1  22943  pntrsumo1  22948  selbergr  22951  pntpbnd1  22969  pntlemk  22989  mideulem  23262  axlowdimlem16  23356  axcontlem8  23370  gxnn0suc  23904  gxinv  23910  vsfval  24166  lnocoi  24310  nmblolbii  24352  ipasslem5  24388  hvsubid  24581  sshjval3  24910  pjhthlem1  24947  adjval  25447  unopf1o  25473  kbpj  25513  lnopmi  25557  nmcoplbi  25585  cnlnadjlem2  25625  adjadd  25650  branmfn  25662  pjtoi  25736  fimacnvinrn2  26105  ofoprabco  26134  xrsmulgzz  26285  xrge0adddir  26301  archiabllem1a  26354  gsumvsca1  26397  gsumvsca2  26398  rdivmuldivd  26405  xrge0iifhom  26513  qqhval2lem  26556  qqhrhm  26564  esumsn  26661  measvunilem0  26773  ballotlemsf1o  27041  ofccat  27086  signstfveq0  27123  igamlgam  27181  lgam1  27195  cvmlift3lem2  27354  cvmlift3lem4  27356  cvmlift3lem5  27357  cvmlift3lem6  27358  cvmlift3lem9  27361  prodmolem3  27591  prodmolem2a  27592  fprodf1o  27604  prodsn  27618  fprodabs  27629  binomfallfac  27689  fallfacval4  27691  bcfallfac  27692  finixpnum  28563  mblfinlem3  28579  dvtan  28591  itg2addnc  28595  itgaddnclem2  28600  ftc1anclem6  28621  areacirclem5  28637  areacirc  28638  upixp  28772  prdsbnd2  28843  ismrer1  28886  rngoneglmul  28906  rngoisocnv  28936  pellexlem2  29320  rmxyneg  29410  oddcomabszz  29434  acongeq  29475  phisum  29716  hausgraph  29729  expgrowth  29758  sumsnd  29897  fmuldfeqlem1  29912  cncfmptss  29917  climexp  29927  stoweidlem17  29961  wallispi  30014  sigarperm  30045  clwlkfoclwwlk  30667  fdmdifeqresdif  30881  lmodvsmmulgdi  30969  lincsum  31096  lincscm  31097  decpmatmul  31260  pm2mpghm  31304  pm2mpmhmlem2  31307  cpmidgsum2  31366  reccot  31422  rectan  31423  cotsqcscsq  31426  bj-bary1lem  32938  islshpsm  32964  lshpnel2N  32969  lfl0f  33053  ldualvsdi1  33127  ldualgrplem  33129  cmtcomlemN  33232  cvlsupr8  33333  pmodl42N  33834  pmapjat1  33836  llnmod2i2  33846  dalawlem2  33855  pmapj2N  33912  idltrn  34133  cdlemc6  34179  cdleme20d  34295  cdleme22e  34327  cdleme22eALTN  34328  cdleme35b  34433  cdleme48fvg  34483  cdlemg4d  34596  cdlemg8a  34610  cdlemg42  34712  cdlemg47a  34717  tendodi1  34767  tendodi2  34768  cdlemk4  34817  cdlemk21N  34856  cdlemk22  34876  cdlemky  34909  cdlemk53b  34939  cdlemk53  34940  cdlemkyyN  34945  erngdvlem3-rN  34981  tendocnv  35005  dia1dim2  35046  dicvaddcl  35174  dihglblem3N  35279  dihmeetlem4preN  35290  dihmeet2  35330  lcfl7lem  35483  baerlem3lem1  35691  baerlem5alem1  35692  mapdh6bN  35721  mapdh6cN  35722  mapdh6dN  35723  hdmap1l6b  35796  hdmap1l6c  35797  hdmap1l6d  35798  hdmap14lem13  35867
  Copyright terms: Public domain W3C validator