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

Theorem 3eqtr4rd 2495
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 2487 . 2  |-  ( ph  ->  D  =  A )
4 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
53, 4eqtr4d 2487 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435
This theorem is referenced by:  csbun  3843  csbcnvgALT  5177  csbres  5266  odi  7230  phplem4  7701  cantnfp1lem3  8102  cantnfp1  8103  cantnfp1lem3OLD  8128  cantnfp1OLD  8129  cardidm  8343  ackbij2lem2  8623  ackbij2lem3  8624  divneg  10246  xadddilem  11497  xadddi2  11500  dfceil2  11950  modlt  11988  modmulnn  11995  seqcaopr3  12124  bcval5  12378  hashgadd  12427  hashun3  12434  seqcoll  12494  swrdccatwrd  12675  cshwmodn  12748  2cshwcom  12766  revco  12782  cshco  12784  cjreb  12938  recj  12939  imcj  12947  imval2  12966  sqrtmul  13075  absmax  13144  amgm2  13184  summolem2a  13519  fsumf1o  13527  sumsn  13545  sumsplit  13565  fsummulc2  13581  binom  13624  bcxmas  13629  incexclem  13630  incexc  13631  expcnv  13657  cvgrat  13674  prodmolem3  13722  prodmolem2a  13723  fprodf1o  13735  prodsn  13749  fprodabs  13760  ege2le3  13807  efaddlem  13810  eftlub  13826  tanval3  13851  tanneg  13865  cosmul  13890  cos01bnd  13903  demoivreALT  13918  absmulgcd  14167  eulerthlem2  14294  pythagtriplem14  14334  pcmul  14357  pcfac  14400  prmreclem6  14421  4sqlem12  14456  vdwlem6  14486  oppccatid  15096  curf2ndf  15495  oppcyon  15517  joincomALT  15638  meetcomALT  15640  pwsco1mhm  15980  sgrp2nmndlem4  16025  mulgnn0p1  16132  mulgneg  16139  mulgnn0dir  16144  qusgrp2  16167  qusghm  16282  gaid  16316  pmtrdifellem3  16482  psgnunilem2  16499  odmulg  16557  sylow1lem2  16598  sylow2a  16618  sylow3lem1  16626  efgredleme  16740  efgcpbllemb  16752  gsumzaddlem  16913  gsumzaddlemOLD  16915  gsumconst  16933  gsumzmhm  16936  gsumzmhmOLD  16937  srgpcomp  17162  srgbinom  17175  lmodvsmmulgdi  17526  lmodsubdi  17546  0lmhm  17665  lspsneq  17747  qusrhm  17864  quscrng  17867  asclrhm  17970  resspsrmul  18051  evlsscasrng  18174  psropprmul  18258  evls1scasrng  18354  zringlpirlem3  18489  zlpirlem3  18494  mulgrhm  18510  mulgrhmOLD  18513  frlmip  18787  frlmphl  18790  mat1ghm  18963  mat1mhm  18964  1marepvmarrepid  19055  mdetrlin  19082  mdetrsca2  19084  mdetunilem7  19098  mdetunilem9  19100  mndifsplit  19116  maducoeval2  19120  smadiadetglem2  19152  decpmatmul  19251  pm2mpghm  19295  pm2mpmhmlem2  19298  cpmidgsum2  19358  ptbasfi  20060  ptuni  20073  alexsubALTlem3  20527  subgtgp  20582  tsmsxplem1  20633  xmsuspOLD  21066  xmsusp  21067  restmetu  21068  nminv  21118  nrginvrcnlem  21177  copco  21496  pcoass  21502  pi1bas  21516  pi1xfrf  21531  pi1xfr  21533  cph2subdi  21634  cphassr  21636  tchcphlem1  21656  rrxip  21800  rrxnm  21801  pjthlem1  21830  ovolunlem1a  21885  ovolfs2  21958  uniiccdif  21965  ismbf  22015  itgaddlem2  22208  ditgswap  22241  ply1divex  22515  plyeq0lem  22585  plymullem1  22589  dgrcolem2  22649  vieta1lem2  22685  elqaalem2  22694  elqaalem3  22695  aaliou3lem7  22723  ulmshft  22763  mulcxplem  23043  cxpmul2  23048  root1eq1  23107  cxpeq  23109  cosangneg2d  23117  isosctrlem2  23131  angpieqvdlem  23137  chordthmlem3  23143  chordthmlem4  23144  chordthmlem5  23145  quad2  23148  dcubic2  23153  cubic2  23157  quart1  23165  scvxcvx  23293  basellem9  23340  ppifl  23412  mumul  23433  sgmmul  23454  chtublem  23464  chpub  23473  logfacrlim  23477  dchrsum2  23521  sumdchr2  23523  bposlem9  23545  lgsdir2  23581  lgsdir  23583  lgsdi  23585  lgsdirnn0  23592  lgsdinn0  23593  lgsquad3  23614  2sqblem  23630  chpo1ub  23643  dchrmusum2  23657  dchrvmasumlem1  23658  dchrvmasum2if  23660  dchrisum0fmul  23669  rpvmasum2  23675  mulog2sumlem1  23697  vmalogdivsum2  23701  log2sumbnd  23707  selberg3lem1  23720  selberg4lem1  23723  pntrsumo1  23728  selbergr  23731  pntpbnd1  23749  pntlemk  23769  tgbtwnconn1lem3  23939  mideulem2  24086  axlowdimlem16  24238  axcontlem8  24252  clwlkfoclwwlk  24823  ex-ind-dvds  25148  gxnn0suc  25244  gxinv  25250  vsfval  25506  lnocoi  25650  nmblolbii  25692  ipasslem5  25728  hvsubid  25921  sshjval3  26250  pjhthlem1  26287  adjval  26787  unopf1o  26813  kbpj  26853  lnopmi  26897  nmcoplbi  26925  cnlnadjlem2  26965  adjadd  26990  branmfn  27002  pjtoi  27076  fimacnvinrn2  27454  ofoprabco  27483  xrsmulgzz  27644  archiabllem1a  27713  gsumvsca1  27751  gsumvsca2  27752  rdivmuldivd  27759  xrge0iifhom  27897  qqhval2lem  27940  qqhrhm  27948  qqhucn  27951  esumsn  28050  measvunilem0  28162  ballotlemsf1o  28430  ofccat  28475  signstfveq0  28512  igamlgam  28570  lgam1  28584  cvmlift3lem2  28743  cvmlift3lem4  28745  cvmlift3lem5  28746  cvmlift3lem6  28747  cvmlift3lem9  28750  elmrsubrn  28858  binomfallfac  29139  fallfacval4  29141  bcfallfac  29142  finixpnum  30014  mblfinlem3  30029  dvtan  30041  itg2addnc  30045  itgaddnclem2  30050  ftc1anclem6  30071  areacirclem5  30087  areacirc  30088  upixp  30196  prdsbnd2  30267  ismrer1  30310  rngoneglmul  30330  rngoisocnv  30360  pellexlem2  30742  rmxyneg  30832  oddcomabszz  30856  acongeq  30897  phisum  31135  hausgraph  31148  expgrowth  31216  sumsnd  31355  sumsnf  31524  fmuldfeqlem1  31530  cncfmptss  31535  prodsnf  31541  climexp  31565  dvresntr  31667  stoweidlem17  31753  wallispi  31806  dirkertrigeq  31837  dirkercncflem2  31840  fourierdlem30  31873  fourierdlem41  31884  fourierdlem81  31924  fourierdlem103  31946  sigarperm  32031  cznrng  32590  rngchomrnghmresOLD  32679  fdmdifeqresdif  32799  lincsum  32900  lincscm  32901  lmod1lem4  32961  reccot  33022  rectan  33023  cotsqcscsq  33026  bj-bary1lem  34554  islshpsm  34580  lshpnel2N  34585  lfl0f  34669  ldualvsdi1  34743  ldualgrplem  34745  cmtcomlemN  34848  cvlsupr8  34949  pmodl42N  35450  pmapjat1  35452  llnmod2i2  35462  dalawlem2  35471  pmapj2N  35528  idltrn  35749  cdlemc6  35796  cdleme20d  35913  cdleme22e  35945  cdleme22eALTN  35946  cdleme35b  36051  cdleme48fvg  36101  cdlemg4d  36214  cdlemg8a  36228  cdlemg42  36330  cdlemg47a  36335  tendodi1  36385  tendodi2  36386  cdlemk4  36435  cdlemk21N  36474  cdlemk22  36494  cdlemky  36527  cdlemk53b  36557  cdlemk53  36558  cdlemkyyN  36563  erngdvlem3-rN  36599  tendocnv  36623  dia1dim2  36664  dicvaddcl  36792  dihglblem3N  36897  dihmeetlem4preN  36908  dihmeet2  36948  lcfl7lem  37101  baerlem3lem1  37309  baerlem5alem1  37310  mapdh6bN  37339  mapdh6cN  37340  mapdh6dN  37341  hdmap1l6b  37414  hdmap1l6c  37415  hdmap1l6d  37416  hdmap14lem13  37485  inductionexd  37771
  Copyright terms: Public domain W3C validator