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

Theorem 3eqtr4rd 2519
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 2511 . 2  |-  ( ph  ->  D  =  A )
4 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
53, 4eqtr4d 2511 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  csbun  3857  csbcnvgALT  5185  csbres  5274  odi  7225  phplem4  7696  cantnfp1lem3  8095  cantnfp1  8096  cantnfp1lem3OLD  8121  cantnfp1OLD  8122  cardidm  8336  ackbij2lem2  8616  ackbij2lem3  8617  divneg  10235  xadddilem  11482  xadddi2  11485  dfceil2  11931  modlt  11969  modmulnn  11976  seqcaopr3  12105  bcval5  12358  hashgadd  12407  hashun3  12414  seqcoll  12472  swrdccatwrd  12650  cshwmodn  12723  2cshwcom  12741  revco  12757  cshco  12759  cjreb  12913  recj  12914  imcj  12922  imval2  12941  sqrtmul  13050  absmax  13118  amgm2  13158  summolem2a  13493  fsumf1o  13501  sumsn  13519  sumsplit  13539  fsummulc2  13555  binom  13598  bcxmas  13603  incexclem  13604  incexc  13605  expcnv  13631  cvgrat  13648  ege2le3  13680  efaddlem  13683  eftlub  13698  tanval3  13723  tanneg  13737  cosmul  13762  cos01bnd  13775  demoivreALT  13790  absmulgcd  14037  eulerthlem2  14164  pythagtriplem14  14204  pcmul  14227  pcfac  14270  prmreclem6  14291  4sqlem12  14326  vdwlem6  14356  oppccatid  14968  curf2ndf  15367  oppcyon  15389  joincomALT  15509  meetcomALT  15511  pwsco1mhm  15808  mulgnn0p1  15950  mulgneg  15957  mulgnn0dir  15962  divsgrp2  15985  divsghm  16095  gaid  16129  pmtrdifellem3  16296  psgnunilem2  16313  odmulg  16371  sylow1lem2  16412  sylow2a  16432  sylow3lem1  16440  efgredleme  16554  efgcpbllemb  16566  gsumzaddlem  16722  gsumzaddlemOLD  16724  gsumconst  16742  gsumzmhm  16745  gsumzmhmOLD  16746  srgpcomp  16968  srgbinom  16981  lmodvsmmulgdi  17327  lmodsubdi  17347  0lmhm  17466  lspsneq  17548  divsrhm  17664  divscrng  17667  asclrhm  17759  resspsrmul  17840  evlsscasrng  17963  psropprmul  18047  evls1scasrng  18143  zringlpirlem3  18275  zlpirlem3  18280  mulgrhm  18296  mulgrhmOLD  18299  frlmip  18573  frlmphl  18576  mat1ghm  18749  mat1mhm  18750  1marepvmarrepid  18841  mdetrlin  18868  mdetrsca2  18870  mdetunilem7  18884  mdetunilem9  18886  mndifsplit  18902  maducoeval2  18906  smadiadetglem2  18938  decpmatmul  19037  pm2mpghm  19081  pm2mpmhmlem2  19084  cpmidgsum2  19144  ptbasfi  19814  ptuni  19827  alexsubALTlem3  20281  subgtgp  20336  tsmsxplem1  20387  xmsuspOLD  20820  xmsusp  20821  restmetu  20822  nminv  20872  nrginvrcnlem  20931  copco  21250  pcoass  21256  pi1bas  21270  pi1xfrf  21285  pi1xfr  21287  cph2subdi  21388  cphassr  21390  tchcphlem1  21410  rrxip  21554  rrxnm  21555  pjthlem1  21584  ovolunlem1a  21639  ovolfs2  21712  uniiccdif  21719  ismbf  21769  itgaddlem2  21962  ditgswap  21995  ply1divex  22269  plyeq0lem  22339  plymullem1  22343  dgrcolem2  22402  vieta1lem2  22438  elqaalem2  22447  elqaalem3  22448  aaliou3lem7  22476  ulmshft  22516  mulcxplem  22790  cxpmul2  22795  root1eq1  22854  cxpeq  22856  cosangneg2d  22864  isosctrlem2  22878  angpieqvdlem  22884  chordthmlem3  22890  chordthmlem4  22891  chordthmlem5  22892  quad2  22895  dcubic2  22900  cubic2  22904  quart1  22912  scvxcvx  23040  basellem9  23087  ppifl  23159  mumul  23180  sgmmul  23201  chtublem  23211  chpub  23220  logfacrlim  23224  dchrsum2  23268  sumdchr2  23270  bposlem9  23292  lgsdir2  23328  lgsdir  23330  lgsdi  23332  lgsdirnn0  23339  lgsdinn0  23340  2sqblem  23377  chpo1ub  23390  dchrmusum2  23404  dchrvmasumlem1  23405  dchrvmasum2if  23407  dchrisum0fmul  23416  rpvmasum2  23422  mulog2sumlem1  23444  vmalogdivsum2  23448  log2sumbnd  23454  selberg3lem1  23467  selberg4lem1  23470  pntrsumo1  23475  selbergr  23478  pntpbnd1  23496  pntlemk  23516  mideulem  23810  axlowdimlem16  23933  axcontlem8  23947  clwlkfoclwwlk  24518  gxnn0suc  24939  gxinv  24945  vsfval  25201  lnocoi  25345  nmblolbii  25387  ipasslem5  25423  hvsubid  25616  sshjval3  25945  pjhthlem1  25982  adjval  26482  unopf1o  26508  kbpj  26548  lnopmi  26592  nmcoplbi  26620  cnlnadjlem2  26660  adjadd  26685  branmfn  26697  pjtoi  26771  fimacnvinrn2  27146  ofoprabco  27174  xrsmulgzz  27325  xrge0adddir  27341  archiabllem1a  27394  gsumvsca1  27433  gsumvsca2  27434  rdivmuldivd  27441  xrge0iifhom  27552  qqhval2lem  27595  qqhrhm  27603  esumsn  27709  measvunilem0  27821  ballotlemsf1o  28089  ofccat  28134  signstfveq0  28171  igamlgam  28229  lgam1  28243  cvmlift3lem2  28402  cvmlift3lem4  28404  cvmlift3lem5  28405  cvmlift3lem6  28406  cvmlift3lem9  28409  prodmolem3  28639  prodmolem2a  28640  fprodf1o  28652  prodsn  28666  fprodabs  28677  binomfallfac  28737  fallfacval4  28739  bcfallfac  28740  finixpnum  29612  mblfinlem3  29628  dvtan  29640  itg2addnc  29644  itgaddnclem2  29649  ftc1anclem6  29670  areacirclem5  29686  areacirc  29687  upixp  29821  prdsbnd2  29892  ismrer1  29935  rngoneglmul  29955  rngoisocnv  29985  pellexlem2  30368  rmxyneg  30458  oddcomabszz  30482  acongeq  30523  phisum  30764  hausgraph  30777  expgrowth  30840  sumsnd  30979  fmuldfeqlem1  31132  cncfmptss  31137  climexp  31147  stoweidlem17  31317  wallispi  31370  dirkercncflem2  31404  fourierdlem30  31437  sigarperm  31544  fdmdifeqresdif  31995  lincsum  32103  lincscm  32104  reccot  32233  rectan  32234  cotsqcscsq  32237  bj-bary1lem  33751  islshpsm  33777  lshpnel2N  33782  lfl0f  33866  ldualvsdi1  33940  ldualgrplem  33942  cmtcomlemN  34045  cvlsupr8  34146  pmodl42N  34647  pmapjat1  34649  llnmod2i2  34659  dalawlem2  34668  pmapj2N  34725  idltrn  34946  cdlemc6  34992  cdleme20d  35108  cdleme22e  35140  cdleme22eALTN  35141  cdleme35b  35246  cdleme48fvg  35296  cdlemg4d  35409  cdlemg8a  35423  cdlemg42  35525  cdlemg47a  35530  tendodi1  35580  tendodi2  35581  cdlemk4  35630  cdlemk21N  35669  cdlemk22  35689  cdlemky  35722  cdlemk53b  35752  cdlemk53  35753  cdlemkyyN  35758  erngdvlem3-rN  35794  tendocnv  35818  dia1dim2  35859  dicvaddcl  35987  dihglblem3N  36092  dihmeetlem4preN  36103  dihmeet2  36143  lcfl7lem  36296  baerlem3lem1  36504  baerlem5alem1  36505  mapdh6bN  36534  mapdh6cN  36535  mapdh6dN  36536  hdmap1l6b  36609  hdmap1l6c  36610  hdmap1l6d  36611  hdmap14lem13  36680
  Copyright terms: Public domain W3C validator