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

Theorem 3eqtr4rd 2479
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 2471 . 2  |-  ( ph  ->  D  =  A )
4 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
53, 4eqtr4d 2471 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  odi  6822  phplem4  7289  cantnfp1lem3  7636  cantnfp1  7637  cardidm  7846  ackbij2lem2  8120  ackbij2lem3  8121  divneg  9709  xadddilem  10873  xadddi2  10876  modlt  11258  modmulnn  11265  seqcaopr3  11358  bcval5  11609  hashgadd  11651  hashun3  11658  seqcoll  11712  revco  11803  cjreb  11928  recj  11929  imcj  11937  imval2  11956  sqrmul  12065  absmax  12133  amgm2  12173  summolem2a  12509  fsumf1o  12517  sumsn  12534  sumsplit  12552  fsummulc2  12567  binom  12609  bcxmas  12615  incexclem  12616  incexc  12617  expcnv  12643  cvgrat  12660  ege2le3  12692  efaddlem  12695  eftlub  12710  tanval3  12735  tanneg  12749  cosmul  12774  cos01bnd  12787  demoivreALT  12802  absmulgcd  13047  eulerthlem2  13171  pythagtriplem14  13202  pcmul  13225  pcfac  13268  prmreclem6  13289  4sqlem12  13324  vdwlem6  13354  oppccatid  13945  curf2ndf  14344  oppcyon  14366  joincomALT  14458  meetcomALT  14460  pwsco1mhm  14769  mulgnn0p1  14901  mulgneg  14908  mulgnn0dir  14913  divsgrp2  14936  divsghm  15042  gaid  15076  odmulg  15192  sylow1lem2  15233  sylow2a  15253  sylow3lem1  15261  efgredleme  15375  efgcpbllemb  15387  gsumzaddlem  15526  gsumconst  15532  gsumzmhm  15533  lmodsubdi  16001  0lmhm  16116  lspsneq  16194  divsrhm  16308  divscrng  16311  asclrhm  16400  resspsrmul  16480  psropprmul  16632  zlpirlem3  16770  mulgrhm  16787  ptbasfi  17613  ptuni  17626  alexsubALTlem3  18080  subgtgp  18135  tsmsxplem1  18182  xmsuspOLD  18615  xmsusp  18616  restmetu  18617  nminv  18667  nrginvrcnlem  18726  copco  19043  pcoass  19049  pi1bas  19063  pi1xfrf  19078  pi1xfr  19080  cph2subdi  19172  cphassr  19174  tchcphlem1  19192  pjthlem1  19338  ovolunlem1a  19392  ovolfs2  19463  uniiccdif  19470  ismbf  19522  itgaddlem2  19715  ditgswap  19746  ply1divex  20059  plyeq0lem  20129  plymullem1  20133  dgrcolem2  20192  vieta1lem2  20228  elqaalem2  20237  elqaalem3  20238  aaliou3lem7  20266  ulmshft  20306  mulcxplem  20575  cxpmul2  20580  root1eq1  20639  cxpeq  20641  cosangneg2d  20649  isosctrlem2  20663  angpieqvdlem  20669  chordthmlem3  20675  chordthmlem4  20676  chordthmlem5  20677  quad2  20679  dcubic2  20684  cubic2  20688  quart1  20696  scvxcvx  20824  basellem9  20871  ppifl  20943  mumul  20964  sgmmul  20985  chtublem  20995  chpub  21004  logfacrlim  21008  dchrsum2  21052  sumdchr2  21054  bposlem9  21076  lgsdir2  21112  lgsdir  21114  lgsdi  21116  lgsdirnn0  21123  lgsdinn0  21124  2sqblem  21161  chpo1ub  21174  dchrmusum2  21188  dchrvmasumlem1  21189  dchrvmasum2if  21191  dchrisum0fmul  21200  rpvmasum2  21206  mulog2sumlem1  21228  vmalogdivsum2  21232  log2sumbnd  21238  selberg3lem1  21251  selberg4lem1  21254  pntrsumo1  21259  selbergr  21262  pntpbnd1  21280  pntlemk  21300  gxnn0suc  21852  gxinv  21858  vsfval  22114  lnocoi  22258  nmblolbii  22300  ipasslem5  22336  hvsubid  22528  sshjval3  22856  pjhthlem1  22893  adjval  23393  unopf1o  23419  kbpj  23459  lnopmi  23503  nmcoplbi  23531  cnlnadjlem2  23571  adjadd  23596  branmfn  23608  pjtoi  23682  csbcnvg  24037  fimacnvinrn2  24048  ofoprabco  24079  xrsmulgzz  24200  rdivmuldivd  24227  xrge0iifhom  24323  qqhval2lem  24365  qqhrhm  24373  esumsn  24456  measvunilem0  24567  ballotlemsf1o  24771  igamlgam  24834  lgam1  24848  cvmlift3lem2  25007  cvmlift3lem4  25009  cvmlift3lem5  25010  cvmlift3lem6  25011  cvmlift3lem9  25014  prodmolem3  25259  prodmolem2a  25260  fprodf1o  25272  prodsn  25286  fprodabs  25297  binomfallfac  25357  fallfacval4  25359  bcfallfac  25360  axlowdimlem16  25896  axcontlem8  25910  mblfinlem3  26245  itg2addnc  26259  itgaddnclem2  26264  ftc1anclem6  26285  areacirclem5  26296  areacirc  26297  upixp  26431  prdsbnd2  26504  ismrer1  26547  rngoneglmul  26567  rngoisocnv  26597  pellexlem2  26893  rmxyneg  26983  oddcomabszz  27007  acongeq  27048  psgnunilem2  27395  phisum  27495  hausgraph  27508  expgrowth  27529  sumsnd  27673  fmuldfeqlem1  27688  cncfmptss  27693  climexp  27707  stoweidlem17  27742  wallispi  27795  sigarperm  27826  2cshw1lem3  28250  2cshw2lem3  28254  2cshwcom  28267  reccot  28501  rectan  28502  cotsqcscsq  28505  islshpsm  29778  lshpnel2N  29783  lfl0f  29867  ldualvsdi1  29941  ldualgrplem  29943  cmtcomlemN  30046  cvlsupr8  30147  pmodl42N  30648  pmapjat1  30650  llnmod2i2  30660  dalawlem2  30669  pmapj2N  30726  idltrn  30947  cdlemc6  30993  cdleme20d  31109  cdleme22e  31141  cdleme22eALTN  31142  cdleme35b  31247  cdleme48fvg  31297  cdlemg4d  31410  cdlemg8a  31424  cdlemg42  31526  cdlemg47a  31531  tendodi1  31581  tendodi2  31582  cdlemk4  31631  cdlemk21N  31670  cdlemk22  31690  cdlemky  31723  cdlemk53b  31753  cdlemk53  31754  cdlemkyyN  31759  erngdvlem3-rN  31795  tendocnv  31819  dia1dim2  31860  dicvaddcl  31988  dihglblem3N  32093  dihmeetlem4preN  32104  dihmeet2  32144  lcfl7lem  32297  baerlem3lem1  32505  baerlem5alem1  32506  mapdh6bN  32535  mapdh6cN  32536  mapdh6dN  32537  hdmap1l6b  32610  hdmap1l6c  32611  hdmap1l6d  32612  hdmap14lem13  32681
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator