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

Theorem 3eqtr4rd 2451
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 2443 . 2  |-  ( ph  ->  D  =  A )
4 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
53, 4eqtr4d 2443 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  odi  6785  phplem4  7252  cantnfp1lem3  7596  cantnfp1  7597  cardidm  7806  ackbij2lem2  8080  ackbij2lem3  8081  divneg  9669  xadddilem  10833  xadddi2  10836  modlt  11217  modmulnn  11224  seqcaopr3  11317  bcval5  11568  hashgadd  11610  hashun3  11617  seqcoll  11671  revco  11762  cjreb  11887  recj  11888  imcj  11896  imval2  11915  sqrmul  12024  absmax  12092  amgm2  12132  summolem2a  12468  fsumf1o  12476  sumsn  12493  sumsplit  12511  fsummulc2  12526  binom  12568  bcxmas  12574  incexclem  12575  incexc  12576  expcnv  12602  cvgrat  12619  ege2le3  12651  efaddlem  12654  eftlub  12669  tanval3  12694  tanneg  12708  cosmul  12733  cos01bnd  12746  demoivreALT  12761  absmulgcd  13006  eulerthlem2  13130  pythagtriplem14  13161  pcmul  13184  pcfac  13227  prmreclem6  13248  4sqlem12  13283  vdwlem6  13313  oppccatid  13904  curf2ndf  14303  oppcyon  14325  joincomALT  14417  meetcomALT  14419  pwsco1mhm  14728  mulgnn0p1  14860  mulgneg  14867  mulgnn0dir  14872  divsgrp2  14895  divsghm  15001  gaid  15035  odmulg  15151  sylow1lem2  15192  sylow2a  15212  sylow3lem1  15220  efgredleme  15334  efgcpbllemb  15346  gsumzaddlem  15485  gsumconst  15491  gsumzmhm  15492  lmodsubdi  15960  0lmhm  16075  lspsneq  16153  divsrhm  16267  divscrng  16270  asclrhm  16359  resspsrmul  16439  psropprmul  16591  zlpirlem3  16729  mulgrhm  16746  ptbasfi  17570  ptuni  17583  alexsubALTlem3  18037  subgtgp  18092  tsmsxplem1  18139  xmsuspOLD  18572  xmsusp  18573  restmetu  18574  nminv  18624  nrginvrcnlem  18683  copco  19000  pcoass  19006  pi1bas  19020  pi1xfrf  19035  pi1xfr  19037  cph2subdi  19129  cphassr  19131  tchcphlem1  19149  pjthlem1  19295  ovolunlem1a  19349  ovolfs2  19420  uniiccdif  19427  ismbf  19479  itgaddlem2  19672  ditgswap  19703  ply1divex  20016  plyeq0lem  20086  plymullem1  20090  dgrcolem2  20149  vieta1lem2  20185  elqaalem2  20194  elqaalem3  20195  aaliou3lem7  20223  ulmshft  20263  mulcxplem  20532  cxpmul2  20537  root1eq1  20596  cxpeq  20598  cosangneg2d  20606  isosctrlem2  20620  angpieqvdlem  20626  chordthmlem3  20632  chordthmlem4  20633  chordthmlem5  20634  quad2  20636  dcubic2  20641  cubic2  20645  quart1  20653  scvxcvx  20781  basellem9  20828  ppifl  20900  mumul  20921  sgmmul  20942  chtublem  20952  chpub  20961  logfacrlim  20965  dchrsum2  21009  sumdchr2  21011  bposlem9  21033  lgsdir2  21069  lgsdir  21071  lgsdi  21073  lgsdirnn0  21080  lgsdinn0  21081  2sqblem  21118  chpo1ub  21131  dchrmusum2  21145  dchrvmasumlem1  21146  dchrvmasum2if  21148  dchrisum0fmul  21157  rpvmasum2  21163  mulog2sumlem1  21185  vmalogdivsum2  21189  log2sumbnd  21195  selberg3lem1  21208  selberg4lem1  21211  pntrsumo1  21216  selbergr  21219  pntpbnd1  21237  pntlemk  21257  gxnn0suc  21809  gxinv  21815  vsfval  22071  lnocoi  22215  nmblolbii  22257  ipasslem5  22293  hvsubid  22485  sshjval3  22813  pjhthlem1  22850  adjval  23350  unopf1o  23376  kbpj  23416  lnopmi  23460  nmcoplbi  23488  cnlnadjlem2  23528  adjadd  23553  branmfn  23565  pjtoi  23639  csbcnvg  23994  fimacnvinrn2  24005  ofoprabco  24036  xrsmulgzz  24157  rdivmuldivd  24184  xrge0iifhom  24280  qqhval2lem  24322  qqhrhm  24330  esumsn  24413  measvunilem0  24524  ballotlemsf1o  24728  igamlgam  24791  lgam1  24805  cvmlift3lem2  24964  cvmlift3lem4  24966  cvmlift3lem5  24967  cvmlift3lem6  24968  cvmlift3lem9  24971  prodmolem3  25216  prodmolem2a  25217  fprodf1o  25229  prodsn  25243  fprodabs  25254  binomfallfaclem2  25311  binomfallfac  25312  axlowdimlem16  25804  axcontlem8  25818  mblfinlem2  26148  itg2addnc  26162  itgaddnclem2  26167  areacirclem6  26190  areacirc  26191  upixp  26325  prdsbnd2  26398  ismrer1  26441  rngoneglmul  26461  rngoisocnv  26491  pellexlem2  26787  rmxyneg  26877  oddcomabszz  26901  acongeq  26942  psgnunilem2  27290  phisum  27390  hausgraph  27403  expgrowth  27424  sumsnd  27568  fmuldfeqlem1  27583  cncfmptss  27588  climexp  27602  stoweidlem17  27637  wallispi  27690  sigarperm  27721  swrdccatin12c  28032  reccot  28219  rectan  28220  cotsqcscsq  28223  islshpsm  29467  lshpnel2N  29472  lfl0f  29556  ldualvsdi1  29630  ldualgrplem  29632  cmtcomlemN  29735  cvlsupr8  29836  pmodl42N  30337  pmapjat1  30339  llnmod2i2  30349  dalawlem2  30358  pmapj2N  30415  idltrn  30636  cdlemc6  30682  cdleme20d  30798  cdleme22e  30830  cdleme22eALTN  30831  cdleme35b  30936  cdleme48fvg  30986  cdlemg4d  31099  cdlemg8a  31113  cdlemg42  31215  cdlemg47a  31220  tendodi1  31270  tendodi2  31271  cdlemk4  31320  cdlemk21N  31359  cdlemk22  31379  cdlemky  31412  cdlemk53b  31442  cdlemk53  31443  cdlemkyyN  31448  erngdvlem3-rN  31484  tendocnv  31508  dia1dim2  31549  dicvaddcl  31677  dihglblem3N  31782  dihmeetlem4preN  31793  dihmeet2  31833  lcfl7lem  31986  baerlem3lem1  32194  baerlem5alem1  32195  mapdh6bN  32224  mapdh6cN  32225  mapdh6dN  32226  hdmap1l6b  32299  hdmap1l6c  32300  hdmap1l6d  32301  hdmap14lem13  32370
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2401
  Copyright terms: Public domain W3C validator