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

Theorem 3eqtr3d 2444
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr3d.1  |-  ( ph  ->  A  =  B )
3eqtr3d.2  |-  ( ph  ->  A  =  C )
3eqtr3d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3eqtr3d  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr3d
StepHypRef Expression
1 3eqtr3d.1 . . 3  |-  ( ph  ->  A  =  B )
2 3eqtr3d.2 . . 3  |-  ( ph  ->  A  =  C )
31, 2eqtr3d 2438 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2438 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  mpteqb  5778  fvmptt  5779  fsnunfv  5892  f1ocnvfv1  5973  f1ocnvfv2  5974  fcof1  5979  weniso  6034  caov12d  6227  caov13d  6229  caov411d  6231  caovmo  6243  grprinvlem  6244  grprinvd  6245  grpridd  6246  onovuni  6563  seqomlem1  6666  seqomlem4  6669  onasuc  6731  onesuc  6733  oeeui  6804  fopwdom  7175  unxpdomlem2  7273  cantnfres  7589  cnfcom2lem  7614  cnfcom2  7615  cardiun  7825  ackbij1lem16  8071  ackbij2lem2  8076  fpwwe2lem6  8466  fpwwe2lem8  8468  canthp1lem2  8484  mul12  9188  mul4  9191  addid1  9202  addcan  9206  addcom  9208  addcomd  9224  add12  9235  ppncan  9299  addsub4  9300  muladd  9422  mulcand  9611  receu  9623  div13  9655  divdivdiv  9671  divcan5  9672  divdiv1  9681  divdiv2  9682  halfaddsub  10157  uzindOLD  10320  xadddi  10830  xov1plusxeqvd  10997  fztp  11058  flzadd  11183  fldiv  11196  modnegd  11236  modsub12d  11238  seqm1  11295  seqcaopr  11315  seqf1o  11319  expsub  11382  zesq  11457  digit1  11468  discr1  11470  discr  11471  facnn2  11530  faclbnd6  11545  hashfz1  11585  hashdom  11608  hashun  11611  hashbclem  11656  hashfac  11662  seqcoll  11667  ccatopth  11731  shftval3  11846  crre  11874  resub  11887  imsub  11895  cjsub  11909  abslem2  12098  sqreulem  12118  climshft2  12331  isercolllem2  12414  iseraltlem2  12431  iseraltlem3  12432  fsumsub  12526  fsumtscopo  12536  fsumtscopo2  12537  hashiun  12556  bcxmas  12570  climcndslem1  12584  climcndslem2  12585  trireciplem  12596  geoser  12601  geo2sum2  12606  sinsub  12724  cossub  12725  rpnnen2lem10  12778  ruclem12  12795  divalglem9  12876  bitsinv1lem  12908  bitsinv1  12909  bitsf1  12913  sadasslem  12937  bitsres  12940  smup1  12956  smumul  12960  modgcd  12991  absmulgcd  13002  gcdmultiplez  13006  eucalg  13033  numdensq  13101  dfphi2  13118  phiprm  13121  fermltl  13128  prmdiveq  13130  odzdvds  13136  coprimeprodsq  13138  pythagtriplem6  13150  pythagtriplem7  13151  pythagtriplem12  13155  pythagtriplem16  13159  pcaddlem  13212  sumhash  13220  pcfac  13223  pockthlem  13228  prmreclem6  13244  4sqlem12  13279  4sqlem15  13282  vdwlem3  13306  vdwlem6  13309  vdwlem9  13312  ramub1lem2  13350  divsaddvallem  13731  xpsaddlem  13755  xpsvsca  13759  mrcun  13802  homfeqval  13878  comfeqval  13889  sectcan  13936  sectco  13937  sectmon  13958  monsect  13959  funcsect  14024  setcmon  14197  resscatc  14215  catciso  14217  evlfcllem  14273  curf2cl  14283  curfcl  14284  yonedalem4c  14329  yonedalem3b  14331  yonedainv  14333  latj12  14480  mnd12g  14655  resmhm  14714  pwsco2mhm  14725  frmdup3  14766  grprcan  14793  grplcan  14812  grpinv11  14815  grpinvnz  14817  grplmulf1o  14820  grpinvpropd  14821  grpinvadd  14822  grpsubsub4  14836  mulgz  14866  mulgdirlem  14869  mulgdir  14870  mulgass  14875  mulgsubdir  14876  mulgpropd  14878  pwsmulg  14887  imasgrp2  14888  isnsg3  14929  nmzsubg  14936  ssnmz  14937  eqger  14945  eqglact  14946  ghminv  14968  conjnmz  14994  subgga  15032  gasubg  15034  galcan  15036  gacan  15037  cntzsubg  15090  cntzmhm  15092  sylow1lem1  15187  sylow2blem2  15210  sylow2blem3  15211  lsmmod  15262  lsmpropd  15264  lsmdisj2  15269  subgdisj1  15278  subgdisj2  15279  efgredleme  15330  efgredlemd  15331  efgredlemc  15332  efgredlem  15334  frgpup3lem  15364  mulgdi  15404  lsm4  15430  cygabl  15455  gsummhm2  15490  gsumpt  15500  gsum2d  15501  dprdfeq0  15535  ablfac1eu  15586  rngcom  15647  isrngd  15653  rnglz  15655  rngrz  15656  rng1eq0  15657  rngmneg1  15660  gsumdixp  15670  unitgrp  15727  irredrmul  15767  drngmul0or  15811  subrginv  15839  subrgunit  15841  srngnvl  15899  srngadd  15900  srngmul  15901  issrngd  15904  lmodvs0  15939  lmodvneg1  15942  lmodcom  15945  lmodsubdi  15956  lmodvsinv  16067  lmodvsinv2  16068  lmhmvsca  16076  lvecvs0or  16135  lvecinv  16140  lspsnvs  16141  lspabs2  16147  lspfixed  16155  lspsolv  16170  unitrrg  16308  asclpropd  16359  psrass1lem  16397  psrlidm  16422  psrridm  16423  mvrf1  16444  mplmon2mul  16516  coe1pwmul  16626  prmirredlem  16728  mulgrhm2  16743  chrrhm  16767  znidomb  16797  ip0r  16823  ipdir  16825  ipdi  16826  ipass  16831  ipassr  16832  phlpropd  16841  ocvpj  16899  restin  17184  cncmp  17409  cmpsublem  17416  conndisj  17432  cnconn  17438  kgencmp2  17531  ufldom  17947  tgplacthmeo  18086  ghmcnp  18097  divstgpopn  18102  divstgphaus  18105  tsmsxplem2  18136  tususp  18255  xpsdsval  18364  blpnfctr  18419  xmssym  18448  ressxms  18508  isngp2  18597  ngppropd  18631  nminvr  18658  blcvx  18782  icccvx  18928  pcohtpylem  18997  pcohtpy  18998  pjthlem1  19291  ovollb2lem  19337  ovolicc2lem1  19366  ovolicc2lem5  19370  volsup  19403  ovolioo  19415  uniiccdif  19423  uniioombllem3  19430  uniioombllem4  19431  vitalilem3  19455  itg1sub  19554  itg2const  19585  iblcnlem1  19632  itgcnlem  19634  itgaddlem2  19668  itgsub  19670  itgabs  19679  ditgsplit  19701  dvmulbr  19778  dvcmul  19783  dvcmulf  19784  dvrec  19794  dvmptres3  19795  dvmptadd  19799  dvmptmul  19800  dvmptres2  19801  dvmptneg  19805  dvmptsub  19806  dvmptcj  19807  dvmptco  19811  dveflem  19816  dvlip  19830  dvlipcn  19831  dvlip2  19832  dvcvx  19857  dvfsumle  19858  dvfsumabs  19860  dvfsumlem1  19863  dvfsumlem2  19864  ftc2  19881  ftc2ditglem  19882  itgparts  19884  itgsubstlem  19885  itgsubst  19886  evlslem1  19889  evlseu  19890  evlssca  19896  evlsvar  19897  pf1ind  19928  fta1glem1  20041  fta1blem  20044  plyeq0lem  20082  plymullem1  20086  coeeulem  20096  coe0  20127  coesub  20128  dvply1  20154  plydivlem4  20166  plyrem  20175  fta1lem  20177  vieta1  20182  plyexmo  20183  elqaalem2  20190  aareccl  20196  aannenlem1  20198  aaliou3lem2  20213  dvtaylp  20239  taylthlem1  20242  radcnvlem1  20282  pserdvlem2  20297  efcvx  20318  ptolemy  20357  tangtx  20366  efif1olem3  20399  efif1olem4  20400  lognegb  20437  efiarg  20455  cosargd  20456  tanarg  20467  logtayl  20504  cxpsub  20526  cxproot  20534  cxpsqr  20547  cxpcn3lem  20584  cxpaddlelem  20588  abscxpbnd  20590  root1eq1  20592  cxpeq  20594  logrec  20614  isosctrlem2  20616  isosctrlem3  20617  isosctr  20618  ssscongptld  20619  chordthmlem  20626  quad2  20632  dcubic1lem  20636  mcubic  20640  cubic2  20641  cubic  20642  dquartlem2  20645  dquart  20646  quart1lem  20648  quart1  20649  asinlem2  20662  asinlem3  20664  asinsin  20685  sinacos  20698  atanlogsublem  20708  efiatan2  20710  2efiatan  20711  tanatan  20712  atantan  20716  atans2  20724  dvatan  20728  atantayl  20730  atantayl2  20731  log2cnv  20737  rlimcnp2  20758  cxplim  20763  cxp2lim  20768  cvxcl  20776  scvxcvx  20777  wilthlem1  20804  wilthlem2  20805  ftalem5  20812  basellem3  20818  basellem5  20820  basellem8  20823  mumullem2  20916  musum  20929  musumsum  20930  muinv  20931  sgmppw  20934  1sgmprm  20936  1sgm2ppw  20937  ppiub  20941  logfac2  20954  chpchtsum  20956  perfectlem1  20966  perfectlem2  20967  dchrn0  20987  dchrfi  20992  dchrabs  20997  dchrptlem1  21001  dchrhash  21008  dchr2sum  21010  sum2dchr  21011  bposlem6  21026  bposlem9  21029  lgsvalmod  21052  lgsdilem  21059  lgsne0  21070  lgssq  21072  lgssq2  21073  lgsqr  21083  lgsdchrval  21084  lgsdchr  21085  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem4  21089  lgsquadlem1  21091  lgsquadlem3  21093  lgsquad3  21098  m1lgs  21099  rplogsumlem1  21131  rplogsumlem2  21132  dchrisumlem2  21137  dchrisum0fno1  21158  rpvmasum2  21159  dchrisum0lem1  21163  dchrisum0lem2  21165  mudivsum  21177  mulog2sumlem1  21181  vmalogdivsum  21186  2vmadivsumlem  21187  logsqvma  21189  selberglem2  21193  selberg2lem  21197  selberg3lem1  21204  selberg4lem1  21207  selberg4  21208  pntrsumo1  21212  selbergr  21215  selberg34r  21218  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntibndlem2  21238  pntlemg  21245  pntlemr  21249  pntlemf  21252  ostthlem1  21274  padicabvcxp  21279  ostth3  21285  cusgrasizeindslem3  21437  grpoidinvlem1  21745  grpoideu  21750  grporcan  21762  grpolcan  21774  grpoasscan1  21778  grpoinvop  21782  grpopnpcan2  21794  gxsuc  21813  gxsub  21817  gxmul  21819  ablo4  21828  subgoinv  21849  ablomul  21896  ghgrp  21909  ghablo  21910  rngolz  21942  rngorz  21943  zerdivemp1  21975  nvadd12  22055  nvscom  22063  nvmul0or  22086  nvz0  22110  smcnlem  22146  ipidsq  22162  sspz  22187  lno0  22210  lnoadd  22212  lnomul  22214  ipasslem3  22287  dipdi  22297  dipassr  22300  dipsubdi  22303  ubthlem2  22326  hvmul0or  22480  hvadd12  22490  hvadd4  22491  hvmulcom  22498  normneg  22599  pjhthlem1  22846  chj12  22989  spanunsni  23034  5oalem2  23110  3oalem2  23118  mayete3iOLD  23184  hoadd4  23240  homul12  23261  hosubdi  23264  honegsubdi  23266  hosub4  23269  adj2  23390  lnopmul  23423  lnopaddi  23427  lnfnaddi  23499  lnfnmuli  23500  cnlnadjlem6  23528  adjeq0  23547  leopmul  23590  opsqrlem1  23596  opsqrlem6  23601  hstnmoc  23679  strlem1  23706  chirredlem3  23848  xaddeq0  24072  bcm1n  24104  divnumden2  24114  xmulcand  24120  xreceu  24121  xrsmulgzz  24153  xrge0adddir  24168  dvrcan5  24182  ofldaddlt  24194  rhmunitinv  24213  qqhval2lem  24318  esummulc1  24424  measxun2  24517  measssd  24522  totprobd  24637  zetacvg  24752  lgamgulmlem4  24769  lgamcvg2  24792  gamp1  24795  subfaclim  24827  cvxscon  24883  rescon  24886  cvmliftmolem1  24921  cvmliftlem7  24931  cvmliftlem13  24936  cvmlift2lem7  24949  cvmlift3lem5  24963  ghomf1olem  25058  fprodm1  25243  fallfacfwd  25303  faclim2  25315  funsseq  25339  brbtwn2  25748  axsegconlem10  25769  ax5seglem3  25774  ax5seglem6  25777  axpaschlem  25783  axeuclidlem  25805  axcontlem2  25808  axcontlem7  25813  axcontlem8  25814  bpolydiflem  26004  bpoly4  26009  fsumcube  26010  itg2addnclem  26155  itg2addnclem3  26157  itgaddnclem2  26163  itgsubnc  26166  iblmulc2nc  26169  itgabsnc  26173  areacirclem2  26181  areacirclem5  26185  areacirc  26187  clsun  26221  topjoin  26284  cocanfo  26309  ablo4pnp  26445  zerdivemp1x  26461  crngm4  26503  crngohomfo  26506  diophrw  26707  eldioph2lem1  26708  pellexlem2  26783  pellexlem6  26787  pellex  26788  pell1234qrne0  26806  pell1234qrreccl  26807  pell1qrgaplem  26826  rmxm1  26887  oddcomabszz  26897  jm2.19lem1  26950  jm3.1lem2  26979  dnnumch3  27012  pwssplit4  27059  uvcresum  27110  lmimlbs  27174  flcidc  27247  psgnunilem2  27286  psgnghm  27305  gsumcom3  27322  hashgcdlem  27384  deg1mhm  27394  dvsconst  27415  dvsid  27416  expgrowth  27420  itgsinexplem1  27615  itgsinexp  27616  stoweidlem1  27617  wallispi2lem2  27688  stirlinglem3  27692  stirlinglem5  27694  stirlinglem10  27699  stirlinglem15  27704  sigaradd  27723  cevathlem1  27724  imarnf1pr  27965  frgrancvvdeq  28145  frgrancvvdgeq  28146  bnj1379  28908  bnj1321  29102  lfl0  29548  lfladd  29549  lflmul  29551  eqlkr3  29584  olm11  29710  latm12  29713  cmtcomlemN  29731  omlspjN  29744  hlatj12  29853  1cvrjat  29957  dalemrotyz  30140  padd12N  30321  pmapjlln1  30337  atmod2i1  30343  pmapocjN  30412  pnonsingN  30415  pexmidN  30451  lhp2at0  30514  lhpelim  30519  ltrncnv  30628  ltrnmw  30633  cdleme7c  30727  cdleme15b  30757  cdlemednpq  30781  cdleme20y  30784  cdleme20m  30805  cdleme22cN  30824  cdleme22d  30825  cdleme23b  30832  cdleme30a  30860  cdleme35h  30938  cdlemeg46frv  31007  cdlemg2fv2  31082  cdlemg2l  31085  cdlemg2m  31086  cdlemg8c  31111  cdlemg10bALTN  31118  cdlemg12  31132  cdlemg13a  31133  cdlemg18c  31162  cdlemg19  31166  trlcoat  31205  cdlemg47  31218  tendo1ne0  31310  cdlemk9  31321  cdlemk9bN  31322  dia2dimlem1  31547  tendolinv  31588  tendorinv  31589  dvhlveclem  31591  doca3N  31610  dihmeetlem7N  31793  dihjatc1  31794  dihmeetlem18N  31807  dochnoncon  31874  dihjatc  31900  dihjatcclem1  31901  dihjatcclem4  31904  dochsnkr  31955  lcfl7lem  31982  lcfl8  31985  lcfl9a  31988  lclkrlem1  31989  lclkrlem2e  31994  lclkrlem2j  31999  lcfrlem1  32025  lcfrlem9  32033  lcfrlem23  32048  lcfrlem31  32056  mapd0  32148  mapdpglem21  32175  baerlem3lem1  32190  baerlem5alem1  32191  mapdindp4  32206  mapdh6gN  32225  hdmap1l6g  32300  hgmapval0  32378  hgmaprnlem1N  32382  hlhilhillem  32446
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