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

Theorem 3eqtr4rd 2496
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 2488 . 2  |-  ( ph  ->  D  =  A )
4 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
53, 4eqtr4d 2488 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-cleq 2444
This theorem is referenced by:  csbun  3798  csbcnvgALT  5019  csbres  5108  odi  7280  phplem4  7754  cantnfp1lem3  8185  cantnfp1  8186  cardidm  8393  ackbij2lem2  8670  ackbij2lem3  8671  divneg  10302  xadddilem  11580  xadddi2  11583  dfceil2  12068  modlt  12107  modmulnn  12114  seqcaopr3  12248  bcval5  12503  hashgadd  12556  hashun3  12563  seqcoll  12627  swrdccatwrd  12824  cshwmodn  12897  2cshwcom  12915  revco  12931  cshco  12933  relexpsucl  13096  cjreb  13186  recj  13187  imcj  13195  imval2  13214  sqrtmul  13323  absmax  13392  amgm2  13432  summolem2a  13781  fsumf1o  13789  sumsn  13807  sumsplit  13829  fsummulc2  13845  binom  13888  bcxmas  13893  incexclem  13894  incexc  13895  expcnv  13922  cvgrat  13939  prodmolem3  13987  prodmolem2a  13988  fprodf1o  14000  prodsn  14016  prodsnf  14018  fprodabs  14028  binomfallfac  14094  fallfacval4  14096  bcfallfac  14097  ege2le3  14144  efaddlem  14147  eftlub  14163  tanval3  14188  tanneg  14202  cosmul  14227  cos01bnd  14240  demoivreALT  14255  absmulgcd  14515  lcmfunsnlem2  14613  eulerthlem2  14730  pythagtriplem14  14778  pcmul  14801  pcfac  14844  prmreclem6  14865  4sqlem12  14900  vdwlem6  14936  oppccatid  15624  curf2ndf  16132  oppcyon  16154  joincomALT  16275  meetcomALT  16277  pwsco1mhm  16617  sgrp2nmndlem4  16662  mulgnn0p1  16769  mulgneg  16776  mulgnn0dir  16781  qusgrp2  16804  qusghm  16919  gaid  16953  pmtrdifellem3  17119  psgnunilem2  17136  odmulg  17207  sylow1lem2  17251  sylow2a  17271  sylow3lem1  17279  efgredleme  17393  efgcpbllemb  17405  gsumzaddlem  17554  gsumconst  17567  gsumzmhm  17570  srgpcomp  17765  srgbinom  17778  lmodvsmmulgdi  18126  lmodsubdi  18145  0lmhm  18263  lspsneq  18345  qusrhm  18461  quscrng  18464  asclrhm  18566  resspsrmul  18641  evlsscasrng  18749  psropprmul  18831  evls1scasrng  18927  zringlpirlem3OLD  19055  zringlpirlem3  19057  mulgrhm  19069  frlmip  19336  frlmphl  19339  mat1ghm  19508  mat1mhm  19509  1marepvmarrepid  19600  mdetrlin  19627  mdetrsca2  19629  mdetunilem7  19643  mdetunilem9  19645  mndifsplit  19661  maducoeval2  19665  smadiadetglem2  19697  decpmatmul  19796  pm2mpghm  19840  pm2mpmhmlem2  19843  cpmidgsum2  19903  ptbasfi  20596  ptuni  20609  alexsubALTlem3  21064  subgtgp  21120  tsmsxplem1  21167  xmsusp  21584  restmetu  21585  nminv  21634  nrginvrcnlem  21693  copco  22049  pcoass  22055  pi1bas  22069  pi1xfrf  22084  pi1xfr  22086  cph2subdi  22187  cphassr  22189  tchcphlem1  22209  rrxip  22349  rrxnm  22350  pjthlem1  22391  ovolunlem1a  22449  ovolfs2  22523  uniiccdif  22535  ismbf  22586  itgaddlem2  22781  ditgswap  22814  ply1divex  23087  plyeq0lem  23164  plymullem1  23168  dgrcolem2  23228  vieta1lem2  23264  elqaalem2  23273  elqaalem3  23274  elqaalem2OLD  23276  elqaalem3OLD  23277  aaliou3lem7  23305  ulmshft  23345  mulcxplem  23629  cxpmul2  23634  root1eq1  23695  cxpeq  23697  logbchbase  23708  cosangneg2d  23736  isosctrlem2  23748  angpieqvdlem  23754  chordthmlem3  23760  chordthmlem4  23761  chordthmlem5  23762  quad2  23765  dcubic2  23770  cubic2  23774  quart1  23782  scvxcvx  23911  igamlgam  23975  lgam1  23989  basellem9  24015  ppifl  24087  mumul  24108  sgmmul  24129  chtublem  24139  chpub  24148  logfacrlim  24152  dchrsum2  24196  sumdchr2  24198  bposlem9  24220  lgsdir2  24256  lgsdir  24258  lgsdi  24260  lgsdirnn0  24267  lgsdinn0  24268  lgsquad3  24289  2sqblem  24305  chpo1ub  24318  dchrmusum2  24332  dchrvmasumlem1  24333  dchrvmasum2if  24335  dchrisum0fmul  24344  rpvmasum2  24350  mulog2sumlem1  24372  vmalogdivsum2  24376  log2sumbnd  24382  selberg3lem1  24395  selberg4lem1  24398  pntrsumo1  24403  selbergr  24406  pntpbnd1  24424  pntlemk  24444  tgbtwnconn1lem3  24619  mideulem2  24776  axlowdimlem16  24987  axcontlem8  25001  clwlkfoclwwlk  25573  ex-ind-dvds  25899  gxnn0suc  25992  gxinv  25998  vsfval  26254  lnocoi  26398  nmblolbii  26440  ipasslem5  26476  hvsubid  26679  sshjval3  27007  pjhthlem1  27044  adjval  27543  unopf1o  27569  kbpj  27609  lnopmi  27653  nmcoplbi  27681  cnlnadjlem2  27721  adjadd  27746  branmfn  27758  pjtoi  27832  fimacnvinrn2  28236  ofoprabco  28267  xrsmulgzz  28440  archiabllem1a  28508  gsumvsca1  28545  gsumvsca2  28546  rdivmuldivd  28554  psgnfzto1stlem  28613  submat1n  28631  submatres  28632  madjusmdetlem3  28655  xrge0iifhom  28743  qqhval2lem  28785  qqhrhm  28793  qqhucn  28796  esumsnf  28885  measvunilem0  29035  carsgclctunlem1  29149  ballotlemsf1o  29346  ballotlemsf1oOLD  29384  ofccat  29429  signstfveq0  29466  cvmlift3lem2  30043  cvmlift3lem4  30045  cvmlift3lem5  30046  cvmlift3lem6  30047  cvmlift3lem9  30050  elmrsubrn  30158  bccolsum  30375  bj-bary1lem  31715  csbdif  31726  finixpnum  31930  poimirlem4  31944  poimirlem16  31956  poimirlem19  31959  poimirlem25  31965  mblfinlem3  31979  dvtan  31992  itg2addnc  31996  itgaddnclem2  32001  ftc1anclem6  32022  areacirclem5  32036  areacirc  32037  upixp  32056  prdsbnd2  32127  ismrer1  32170  rngoneglmul  32190  rngoisocnv  32220  islshpsm  32546  lshpnel2N  32551  lfl0f  32635  ldualvsdi1  32709  ldualgrplem  32711  cmtcomlemN  32814  cvlsupr8  32915  pmodl42N  33416  pmapjat1  33418  llnmod2i2  33428  dalawlem2  33437  pmapj2N  33494  idltrn  33715  cdlemc6  33762  cdleme20d  33879  cdleme22e  33911  cdleme22eALTN  33912  cdleme35b  34017  cdleme48fvg  34067  cdlemg4d  34180  cdlemg8a  34194  cdlemg42  34296  cdlemg47a  34301  tendodi1  34351  tendodi2  34352  cdlemk4  34401  cdlemk21N  34440  cdlemk22  34460  cdlemky  34493  cdlemk53b  34523  cdlemk53  34524  cdlemkyyN  34529  erngdvlem3-rN  34565  tendocnv  34589  dia1dim2  34630  dicvaddcl  34758  dihglblem3N  34863  dihmeetlem4preN  34874  dihmeet2  34914  lcfl7lem  35067  baerlem3lem1  35275  baerlem5alem1  35276  mapdh6bN  35305  mapdh6cN  35306  mapdh6dN  35307  hdmap1l6b  35380  hdmap1l6c  35381  hdmap1l6d  35382  hdmap14lem13  35451  pellexlem2  35674  rmxyneg  35768  oddcomabszz  35792  acongeq  35833  phisum  36076  hausgraph  36089  inductionexd  36593  expgrowth  36684  binomcxplemwb  36697  binomcxplemnn0  36698  binomcxplemnotnn0  36705  sumsnd  37347  sumsnf  37648  fmuldfeqlem1  37660  cncfmptss  37665  climexp  37683  dvresntr  37788  stoweidlem17  37877  wallispi  37932  dirkertrigeq  37963  dirkercncflem2  37966  fourierdlem30  37999  fourierdlem41  38011  fourierdlem81  38051  fourierdlem103  38073  sge0xp  38271  sge0isummpt2  38274  isomennd  38352  sigarperm  38469  opoeALTV  38812  c0mgm  39962  c0mhm  39963  zrrnghm  39970  cznrng  40010  rngchomrnghmresALTV  40051  fdmdifeqresdif  40176  lincsum  40275  lincscm  40276  lmod1lem4  40336  blennngt2o2  40456  blennn0e2  40458  reccot  40531  rectan  40532  cotsqcscsq  40535
  Copyright terms: Public domain W3C validator