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

Theorem 3eqtr3d 2325
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 2319 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2319 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1625
This theorem is referenced by:  mpteqb  5616  fvmptt  5617  fsnunfv  5722  f1ocnvfv1  5794  f1ocnvfv2  5795  fcof1  5799  weniso  5854  caov12d  6043  caov13d  6045  caov411d  6047  caovmo  6059  grprinvlem  6060  grprinvd  6061  grpridd  6062  onovuni  6361  seqomlem1  6464  seqomlem4  6467  onasuc  6529  onesuc  6531  oeeui  6602  fopwdom  6972  unxpdomlem2  7070  cantnfres  7381  cnfcom2lem  7406  cnfcom2  7407  cardiun  7617  ackbij1lem16  7863  ackbij2lem2  7868  fpwwe2lem6  8259  fpwwe2lem8  8261  canthp1lem2  8277  mul12  8980  mul4  8983  addid1  8994  addcan  8998  addcom  9000  addcomd  9016  add12  9027  ppncan  9091  addsub4  9092  muladd  9214  mulcand  9403  receu  9415  div13  9447  divdivdiv  9463  divcan5  9464  divdiv1  9473  divdiv2  9474  halfaddsub  9947  uzindOLD  10108  xadddi  10617  xov1plusxeqvd  10782  fztp  10843  flzadd  10953  fldiv  10966  modnegd  11006  modsub12d  11008  seqm1  11065  seqcaopr  11085  seqf1o  11089  expsub  11151  zesq  11226  digit1  11237  discr1  11239  discr  11240  facnn2  11299  faclbnd6  11314  hashfz1  11347  hashdom  11363  hashun  11366  hashbclem  11392  hashfac  11398  seqcoll  11403  ccatopth  11464  shftval3  11573  crre  11601  resub  11614  imsub  11622  cjsub  11636  abslem2  11825  sqreulem  11845  climshft2  12058  isercolllem2  12141  iseraltlem2  12157  iseraltlem3  12158  fsumsub  12252  fsumtscopo  12262  fsumtscopo2  12263  hashiun  12282  bcxmas  12296  climcndslem1  12310  climcndslem2  12311  trireciplem  12322  geoser  12327  geo2sum2  12332  sinsub  12450  cossub  12451  rpnnen2lem10  12504  ruclem12  12521  divalglem9  12602  bitsinv1lem  12634  bitsinv1  12635  bitsf1  12639  sadasslem  12663  bitsres  12666  smup1  12682  smumul  12686  modgcd  12717  absmulgcd  12728  gcdmultiplez  12732  eucalg  12759  numdensq  12827  dfphi2  12844  phiprm  12847  fermltl  12854  prmdiveq  12856  odzdvds  12862  coprimeprodsq  12864  pythagtriplem6  12876  pythagtriplem7  12877  pythagtriplem12  12881  pythagtriplem16  12885  pcaddlem  12938  sumhash  12946  pcfac  12949  pockthlem  12954  prmreclem6  12970  4sqlem12  13005  4sqlem15  13008  vdwlem3  13032  vdwlem6  13035  vdwlem9  13038  ramub1lem2  13076  divsaddvallem  13455  xpsaddlem  13479  xpsvsca  13483  mrcun  13526  homfeqval  13602  comfeqval  13613  sectcan  13660  sectco  13661  sectmon  13682  monsect  13683  funcsect  13748  setcmon  13921  resscatc  13939  catciso  13941  evlfcllem  13997  curf2cl  14007  curfcl  14008  yonedalem4c  14053  yonedalem3b  14055  yonedainv  14057  latj12  14204  mnd12g  14379  resmhm  14438  pwsco2mhm  14449  frmdup3  14490  grprcan  14517  grplcan  14536  grpinv11  14539  grpinvnz  14541  grplmulf1o  14544  grpinvpropd  14545  grpinvadd  14546  grpsubsub4  14560  mulgz  14590  mulgdirlem  14593  mulgdir  14594  mulgass  14599  mulgsubdir  14600  mulgpropd  14602  pwsmulg  14611  imasgrp2  14612  isnsg3  14653  nmzsubg  14660  ssnmz  14661  eqger  14669  eqglact  14670  ghminv  14692  conjnmz  14718  subgga  14756  gasubg  14758  galcan  14760  gacan  14761  cntzsubg  14814  cntzmhm  14816  sylow1lem1  14911  sylow2blem2  14934  sylow2blem3  14935  lsmmod  14986  lsmpropd  14988  lsmdisj2  14993  subgdisj1  15002  subgdisj2  15003  efgredleme  15054  efgredlemd  15055  efgredlemc  15056  efgredlem  15058  frgpup3lem  15088  mulgdi  15128  lsm4  15154  cygabl  15179  gsummhm2  15214  gsumpt  15224  gsum2d  15225  dprdfeq0  15259  ablfac1eu  15310  rngcom  15371  isrngd  15377  rnglz  15379  rngrz  15380  rng1eq0  15381  rngmneg1  15384  gsumdixp  15394  unitgrp  15451  irredrmul  15491  drngmul0or  15535  subrginv  15563  subrgunit  15565  srngnvl  15623  srngadd  15624  srngmul  15625  issrngd  15628  lmodvs0  15666  lmodvneg1  15669  lmodvsnegOLD  15670  lmodcom  15673  lmodsubdi  15684  lmodvsinv  15795  lmodvsinv2  15796  lmhmvsca  15804  lvecvs0or  15863  lvecinv  15868  lspsnvs  15869  lspabs2  15875  lspfixed  15883  lspsolv  15898  unitrrg  16036  asclpropd  16087  psrass1lem  16125  psrlidm  16150  psrridm  16151  mvrf1  16172  mplmon2mul  16244  coe1pwmul  16357  prmirredlem  16448  mulgrhm2  16463  chrrhm  16487  znidomb  16517  ip0r  16543  ipdir  16545  ipdi  16546  ipass  16551  ipassr  16552  phlpropd  16561  ocvpj  16619  restin  16899  cncmp  17121  cmpsublem  17128  conndisj  17144  cnconn  17150  kgencmp2  17243  ufldom  17659  tgplacthmeo  17788  ghmcnp  17799  divstgpopn  17804  divstgphaus  17807  tsmsxplem2  17838  xpsdsval  17947  blpnfctr  17984  xmssym  18013  ressxms  18073  isngp2  18121  ngppropd  18155  nminvr  18182  blcvx  18306  icccvx  18450  pcohtpylem  18519  pcohtpy  18520  pjthlem1  18803  ovollb2lem  18849  ovolicc2lem1  18878  ovolicc2lem5  18882  volsup  18915  ovolioo  18927  uniiccdif  18935  uniioombllem3  18942  uniioombllem4  18943  vitalilem3  18967  itg1sub  19066  itg2const  19097  iblcnlem1  19144  itgcnlem  19146  itgaddlem2  19180  itgsub  19182  itgabs  19191  ditgsplit  19213  dvmulbr  19290  dvcmul  19295  dvcmulf  19296  dvrec  19306  dvmptres3  19307  dvmptadd  19311  dvmptmul  19312  dvmptres2  19313  dvmptneg  19317  dvmptsub  19318  dvmptcj  19319  dvmptco  19323  dveflem  19328  dvlip  19342  dvlipcn  19343  dvlip2  19344  dvcvx  19369  dvfsumle  19370  dvfsumabs  19372  dvfsumlem1  19375  dvfsumlem2  19376  ftc2  19393  ftc2ditglem  19394  itgparts  19396  itgsubstlem  19397  itgsubst  19398  evlslem1  19401  evlseu  19402  evlssca  19408  evlsvar  19409  pf1ind  19440  fta1glem1  19553  fta1blem  19556  plyeq0lem  19594  plymullem1  19598  coeeulem  19608  coe0  19639  coesub  19640  dvply1  19666  plydivlem4  19678  plyrem  19687  fta1lem  19689  vieta1  19694  plyexmo  19695  elqaalem2  19702  aareccl  19708  aannenlem1  19710  aaliou3lem2  19725  dvtaylp  19751  taylthlem1  19754  radcnvlem1  19791  pserdvlem2  19806  efcvx  19827  tangtx  19875  efif1olem3  19908  efif1olem4  19909  lognegb  19945  efiarg  19963  cosargd  19964  tanarg  19972  logtayl  20009  cxpsub  20031  cxproot  20039  cxpsqr  20052  cxpcn3lem  20089  cxpaddlelem  20093  abscxpbnd  20095  root1eq1  20097  cxpeq  20099  logrec  20119  isosctrlem2  20121  isosctrlem3  20122  isosctr  20123  ssscongptld  20124  chordthmlem  20131  quad2  20137  dcubic1lem  20141  mcubic  20145  cubic2  20146  cubic  20147  dquartlem2  20150  dquart  20151  quart1lem  20153  quart1  20154  asinlem2  20167  asinlem3  20169  asinsin  20190  sinacos  20203  atanlogsublem  20213  efiatan2  20215  2efiatan  20216  tanatan  20217  atantan  20221  atans2  20229  dvatan  20233  atantayl  20235  atantayl2  20236  log2cnv  20242  rlimcnp2  20263  cxplim  20268  cxp2lim  20273  cvxcl  20281  scvxcvx  20282  wilthlem1  20308  wilthlem2  20309  ftalem5  20316  basellem3  20322  basellem5  20324  basellem8  20327  mumullem2  20420  musum  20433  musumsum  20434  muinv  20435  sgmppw  20438  1sgmprm  20440  1sgm2ppw  20441  ppiub  20445  logfac2  20458  chpchtsum  20460  perfectlem1  20470  perfectlem2  20471  dchrn0  20491  dchrfi  20496  dchrabs  20501  dchrptlem1  20505  dchrhash  20512  dchr2sum  20514  sum2dchr  20515  bposlem6  20530  bposlem9  20533  lgsvalmod  20556  lgsdilem  20563  lgsne0  20574  lgssq  20576  lgssq2  20577  lgsqr  20587  lgsdchrval  20588  lgsdchr  20589  lgseisenlem1  20590  lgseisenlem2  20591  lgseisenlem4  20593  lgsquadlem1  20595  lgsquadlem3  20597  lgsquad3  20602  m1lgs  20603  rplogsumlem1  20635  rplogsumlem2  20636  dchrisumlem2  20641  dchrisum0fno1  20662  rpvmasum2  20663  dchrisum0lem1  20667  dchrisum0lem2  20669  mudivsum  20681  mulog2sumlem1  20685  vmalogdivsum  20690  2vmadivsumlem  20691  logsqvma  20693  selberglem2  20697  selberg2lem  20701  selberg3lem1  20708  selberg4lem1  20711  selberg4  20712  pntrsumo1  20716  selbergr  20719  selberg34r  20722  pntrlog2bndlem3  20730  pntrlog2bndlem4  20731  pntibndlem2  20742  pntlemg  20749  pntlemr  20753  pntlemf  20756  ostthlem1  20778  padicabvcxp  20783  ostth3  20789  grpoidinvlem1  20873  grpoideu  20878  grporcan  20890  grpolcan  20902  grpoasscan1  20906  grpoinvop  20910  grpopnpcan2  20922  gxsuc  20941  gxsub  20945  gxmul  20947  ablo4  20956  subgoinv  20977  ablomul  21024  ghgrp  21037  ghablo  21038  rngolz  21070  rngorz  21071  nvadd12  21181  nvscom  21189  nvmul0or  21212  nvz0  21236  smcnlem  21272  ipidsq  21288  sspz  21313  lno0  21336  lnoadd  21338  lnomul  21340  ipasslem3  21413  dipdi  21423  dipassr  21426  dipsubdi  21429  ubthlem2  21452  hvmul0or  21606  hvadd12  21616  hvadd4  21617  hvmulcom  21624  normneg  21725  pjhthlem1  21972  chj12  22115  spanunsni  22160  5oalem2  22236  3oalem2  22244  mayete3iOLD  22310  hoadd4  22366  homul12  22387  hosubdi  22390  honegsubdi  22392  hosub4  22395  adj2  22516  lnopmul  22549  lnopaddi  22553  lnfnaddi  22625  lnfnmuli  22626  cnlnadjlem6  22654  adjeq0  22673  leopmul  22716  opsqrlem1  22722  opsqrlem6  22727  hstnmoc  22805  strlem1  22832  chirredlem3  22974  bcm1n  23034  xmulcand  23106  xreceu  23107  xaddeq0  23306  xrsmulgzz  23309  xrge0adddir  23334  esummulc1  23451  measxun2  23540  measssd  23545  totprobd  23631  zetacvg  23691  subfaclim  23721  cvxscon  23776  rescon  23779  cvmliftmolem1  23814  cvmliftlem7  23824  cvmliftlem13  23829  cvmlift2lem7  23842  cvmlift3lem5  23856  ghomf1olem  24003  funsseq  24127  brbtwn2  24535  axsegconlem10  24556  ax5seglem3  24561  ax5seglem6  24564  axpaschlem  24570  axeuclidlem  24592  axcontlem2  24595  axcontlem7  24600  axcontlem8  24601  bpolydiflem  24791  bpoly4  24796  fsumcube  24797  itg2addnclem  24933  itg2addnc  24935  areacirclem2  24936  areacirclem5  24940  areacirc  24942  multinvb  25434  zerdivemp1  25447  mslb1  25618  trnij  25626  addcanrg  25678  idsubfun  25869  clsun  26257  topjoin  26325  cocanfo  26385  ablo4pnp  26581  zerdivemp1x  26597  crngm4  26639  crngohomfo  26642  diophrw  26849  eldioph2lem1  26850  pellexlem2  26926  pellexlem6  26930  pellex  26931  pell1234qrne0  26949  pell1234qrreccl  26950  pell1qrgaplem  26969  rmxm1  27030  oddcomabszz  27040  jm2.19lem1  27093  jm3.1lem2  27122  dnnumch3  27155  pwssplit4  27202  uvcresum  27253  lmimlbs  27317  flcidc  27390  psgnunilem2  27429  psgnghm  27448  gsumcom3  27465  hashgcdlem  27527  deg1mhm  27537  dvsconst  27558  dvsid  27559  expgrowth  27563  itgsinexplem1  27759  sigaradd  27867  cevathlem1  27868  bnj1379  28936  bnj1321  29130  lfl0  29328  lfladd  29329  lflmul  29331  eqlkr3  29364  olm11  29490  latm12  29493  cmtcomlemN  29511  omlspjN  29524  hlatj12  29633  1cvrjat  29737  dalemrotyz  29920  padd12N  30101  pmapjlln1  30117  atmod2i1  30123  pmapocjN  30192  pnonsingN  30195  pexmidN  30231  lhp2at0  30294  lhpelim  30299  ltrncnv  30408  ltrnmw  30413  cdleme7c  30507  cdleme15b  30537  cdlemednpq  30561  cdleme20y  30564  cdleme20m  30585  cdleme22cN  30604  cdleme22d  30605  cdleme23b  30612  cdleme30a  30640  cdleme35h  30718  cdlemeg46frv  30787  cdlemg2fv2  30862  cdlemg2l  30865  cdlemg2m  30866  cdlemg8c  30891  cdlemg10bALTN  30898  cdlemg12  30912  cdlemg13a  30913  cdlemg18c  30942  cdlemg19  30946  trlcoat  30985  cdlemg47  30998  tendo1ne0  31090  cdlemk9  31101  cdlemk9bN  31102  dia2dimlem1  31327  tendolinv  31368  tendorinv  31369  dvhlveclem  31371  doca3N  31390  dihmeetlem7N  31573  dihjatc1  31574  dihmeetlem18N  31587  dochnoncon  31654  dihjatc  31680  dihjatcclem1  31681  dihjatcclem4  31684  dochsnkr  31735  lcfl7lem  31762  lcfl8  31765  lcfl9a  31768  lclkrlem1  31769  lclkrlem2e  31774  lclkrlem2j  31779  lcfrlem1  31805  lcfrlem9  31813  lcfrlem23  31828  lcfrlem31  31836  mapd0  31928  mapdpglem21  31955  baerlem3lem1  31970  baerlem5alem1  31971  mapdindp4  31986  mapdh6gN  32005  hdmap1l6g  32080  hgmapval0  32158  hgmaprnlem1N  32162  hlhilhillem  32226
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-cleq 2278
  Copyright terms: Public domain W3C validator