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

Theorem 3eqtr4rd 2447
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 2439 . 2  |-  ( ph  ->  D  =  A )
4 3eqtr4d.2 . 2  |-  ( ph  ->  C  =  A )
53, 4eqtr4d 2439 1  |-  ( ph  ->  D  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  odi  6781  phplem4  7248  cantnfp1lem3  7592  cantnfp1  7593  cardidm  7802  ackbij2lem2  8076  ackbij2lem3  8077  divneg  9665  xadddilem  10829  xadddi2  10832  modlt  11213  modmulnn  11220  seqcaopr3  11313  bcval5  11564  hashgadd  11606  hashun3  11613  seqcoll  11667  revco  11758  cjreb  11883  recj  11884  imcj  11892  imval2  11911  sqrmul  12020  absmax  12088  amgm2  12128  summolem2a  12464  fsumf1o  12472  sumsn  12489  sumsplit  12507  fsummulc2  12522  binom  12564  bcxmas  12570  incexclem  12571  incexc  12572  expcnv  12598  cvgrat  12615  ege2le3  12647  efaddlem  12650  eftlub  12665  tanval3  12690  tanneg  12704  cosmul  12729  cos01bnd  12742  demoivreALT  12757  absmulgcd  13002  eulerthlem2  13126  pythagtriplem14  13157  pcmul  13180  pcfac  13223  prmreclem6  13244  4sqlem12  13279  vdwlem6  13309  oppccatid  13900  curf2ndf  14299  oppcyon  14321  joincomALT  14413  meetcomALT  14415  pwsco1mhm  14724  mulgnn0p1  14856  mulgneg  14863  mulgnn0dir  14868  divsgrp2  14891  divsghm  14997  gaid  15031  odmulg  15147  sylow1lem2  15188  sylow2a  15208  sylow3lem1  15216  efgredleme  15330  efgcpbllemb  15342  gsumzaddlem  15481  gsumconst  15487  gsumzmhm  15488  lmodsubdi  15956  0lmhm  16071  lspsneq  16149  divsrhm  16263  divscrng  16266  asclrhm  16355  resspsrmul  16435  psropprmul  16587  zlpirlem3  16725  mulgrhm  16742  ptbasfi  17566  ptuni  17579  alexsubALTlem3  18033  subgtgp  18088  tsmsxplem1  18135  xmsuspOLD  18568  xmsusp  18569  restmetu  18570  nminv  18620  nrginvrcnlem  18679  copco  18996  pcoass  19002  pi1bas  19016  pi1xfrf  19031  pi1xfr  19033  cph2subdi  19125  cphassr  19127  tchcphlem1  19145  pjthlem1  19291  ovolunlem1a  19345  ovolfs2  19416  uniiccdif  19423  ismbf  19475  itgaddlem2  19668  ditgswap  19699  ply1divex  20012  plyeq0lem  20082  plymullem1  20086  dgrcolem2  20145  vieta1lem2  20181  elqaalem2  20190  elqaalem3  20191  aaliou3lem7  20219  ulmshft  20259  mulcxplem  20528  cxpmul2  20533  root1eq1  20592  cxpeq  20594  cosangneg2d  20602  isosctrlem2  20616  angpieqvdlem  20622  chordthmlem3  20628  chordthmlem4  20629  chordthmlem5  20630  quad2  20632  dcubic2  20637  cubic2  20641  quart1  20649  scvxcvx  20777  basellem9  20824  ppifl  20896  mumul  20917  sgmmul  20938  chtublem  20948  chpub  20957  logfacrlim  20961  dchrsum2  21005  sumdchr2  21007  bposlem9  21029  lgsdir2  21065  lgsdir  21067  lgsdi  21069  lgsdirnn0  21076  lgsdinn0  21077  2sqblem  21114  chpo1ub  21127  dchrmusum2  21141  dchrvmasumlem1  21142  dchrvmasum2if  21144  dchrisum0fmul  21153  rpvmasum2  21159  mulog2sumlem1  21181  vmalogdivsum2  21185  log2sumbnd  21191  selberg3lem1  21204  selberg4lem1  21207  pntrsumo1  21212  selbergr  21215  pntpbnd1  21233  pntlemk  21253  gxnn0suc  21805  gxinv  21811  vsfval  22067  lnocoi  22211  nmblolbii  22253  ipasslem5  22289  hvsubid  22481  sshjval3  22809  pjhthlem1  22846  adjval  23346  unopf1o  23372  kbpj  23412  lnopmi  23456  nmcoplbi  23484  cnlnadjlem2  23524  adjadd  23549  branmfn  23561  pjtoi  23635  csbcnvg  23990  fimacnvinrn2  24001  ofoprabco  24032  xrsmulgzz  24153  rdivmuldivd  24180  xrge0iifhom  24276  qqhval2lem  24318  qqhrhm  24326  esumsn  24409  measvunilem0  24520  ballotlemsf1o  24724  igamlgam  24787  lgam1  24801  cvmlift3lem2  24960  cvmlift3lem4  24962  cvmlift3lem5  24963  cvmlift3lem6  24964  cvmlift3lem9  24967  prodmolem3  25212  prodmolem2a  25213  fprodf1o  25225  prodsn  25239  fprodabs  25250  binomfallfaclem2  25307  binomfallfac  25308  axlowdimlem16  25800  axcontlem8  25814  mblfinlem2  26144  itg2addnc  26158  itgaddnclem2  26163  areacirclem6  26186  areacirc  26187  upixp  26321  prdsbnd2  26394  ismrer1  26437  rngoneglmul  26457  rngoisocnv  26487  pellexlem2  26783  rmxyneg  26873  oddcomabszz  26897  acongeq  26938  psgnunilem2  27286  phisum  27386  hausgraph  27399  expgrowth  27420  sumsnd  27564  fmuldfeqlem1  27579  cncfmptss  27584  climexp  27598  stoweidlem17  27633  wallispi  27686  sigarperm  27717  swrdccatin12c  28028  reccot  28215  rectan  28216  cotsqcscsq  28219  islshpsm  29463  lshpnel2N  29468  lfl0f  29552  ldualvsdi1  29626  ldualgrplem  29628  cmtcomlemN  29731  cvlsupr8  29832  pmodl42N  30333  pmapjat1  30335  llnmod2i2  30345  dalawlem2  30354  pmapj2N  30411  idltrn  30632  cdlemc6  30678  cdleme20d  30794  cdleme22e  30826  cdleme22eALTN  30827  cdleme35b  30932  cdleme48fvg  30982  cdlemg4d  31095  cdlemg8a  31109  cdlemg42  31211  cdlemg47a  31216  tendodi1  31266  tendodi2  31267  cdlemk4  31316  cdlemk21N  31355  cdlemk22  31375  cdlemky  31408  cdlemk53b  31438  cdlemk53  31439  cdlemkyyN  31444  erngdvlem3-rN  31480  tendocnv  31504  dia1dim2  31545  dicvaddcl  31673  dihglblem3N  31778  dihmeetlem4preN  31789  dihmeet2  31829  lcfl7lem  31982  baerlem3lem1  32190  baerlem5alem1  32191  mapdh6bN  32220  mapdh6cN  32221  mapdh6dN  32222  hdmap1l6b  32295  hdmap1l6c  32296  hdmap1l6d  32297  hdmap14lem13  32366
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 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator