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

Theorem 3eqtr3d 2323
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 2317 . 2  |-  ( ph  ->  B  =  C )
4 3eqtr3d.3 . 2  |-  ( ph  ->  B  =  D )
53, 4eqtr3d 2317 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  mpteqb  5614  fvmptt  5615  fsnunfv  5720  f1ocnvfv1  5792  f1ocnvfv2  5793  fcof1  5797  weniso  5852  caov12d  6041  caov13d  6043  caov411d  6045  caovmo  6057  grprinvlem  6058  grprinvd  6059  grpridd  6060  onovuni  6359  seqomlem1  6462  seqomlem4  6465  onasuc  6527  onesuc  6529  oeeui  6600  fopwdom  6970  unxpdomlem2  7068  cantnfres  7379  cnfcom2lem  7404  cnfcom2  7405  cardiun  7615  ackbij1lem16  7861  ackbij2lem2  7866  fpwwe2lem6  8257  fpwwe2lem8  8259  canthp1lem2  8275  mul12  8978  mul4  8981  addid1  8992  addcan  8996  addcom  8998  addcomd  9014  add12  9025  ppncan  9089  addsub4  9090  muladd  9212  mulcand  9401  receu  9413  div13  9445  divdivdiv  9461  divcan5  9462  divdiv1  9471  divdiv2  9472  halfaddsub  9945  uzindOLD  10106  xadddi  10615  xov1plusxeqvd  10780  fztp  10841  flzadd  10951  fldiv  10964  modnegd  11004  modsub12d  11006  seqm1  11063  seqcaopr  11083  seqf1o  11087  expsub  11149  zesq  11224  digit1  11235  discr1  11237  discr  11238  facnn2  11297  faclbnd6  11312  hashfz1  11345  hashdom  11361  hashun  11364  hashbclem  11390  hashfac  11396  seqcoll  11401  ccatopth  11462  shftval3  11571  crre  11599  resub  11612  imsub  11620  cjsub  11634  abslem2  11823  sqreulem  11843  climshft2  12056  isercolllem2  12139  iseraltlem2  12155  iseraltlem3  12156  fsumsub  12250  fsumtscopo  12260  fsumtscopo2  12261  hashiun  12280  bcxmas  12294  climcndslem1  12308  climcndslem2  12309  trireciplem  12320  geoser  12325  geo2sum2  12330  sinsub  12448  cossub  12449  rpnnen2lem10  12502  ruclem12  12519  divalglem9  12600  bitsinv1lem  12632  bitsinv1  12633  bitsf1  12637  sadasslem  12661  bitsres  12664  smup1  12680  smumul  12684  modgcd  12715  absmulgcd  12726  gcdmultiplez  12730  eucalg  12757  numdensq  12825  dfphi2  12842  phiprm  12845  fermltl  12852  prmdiveq  12854  odzdvds  12860  coprimeprodsq  12862  pythagtriplem6  12874  pythagtriplem7  12875  pythagtriplem12  12879  pythagtriplem16  12883  pcaddlem  12936  sumhash  12944  pcfac  12947  pockthlem  12952  prmreclem6  12968  4sqlem12  13003  4sqlem15  13006  vdwlem3  13030  vdwlem6  13033  vdwlem9  13036  ramub1lem2  13074  divsaddvallem  13453  xpsaddlem  13477  xpsvsca  13481  mrcun  13524  homfeqval  13600  comfeqval  13611  sectcan  13658  sectco  13659  sectmon  13680  monsect  13681  funcsect  13746  setcmon  13919  resscatc  13937  catciso  13939  evlfcllem  13995  curf2cl  14005  curfcl  14006  yonedalem4c  14051  yonedalem3b  14053  yonedainv  14055  latj12  14202  mnd12g  14377  resmhm  14436  pwsco2mhm  14447  frmdup3  14488  grprcan  14515  grplcan  14534  grpinv11  14537  grpinvnz  14539  grplmulf1o  14542  grpinvpropd  14543  grpinvadd  14544  grpsubsub4  14558  mulgz  14588  mulgdirlem  14591  mulgdir  14592  mulgass  14597  mulgsubdir  14598  mulgpropd  14600  pwsmulg  14609  imasgrp2  14610  isnsg3  14651  nmzsubg  14658  ssnmz  14659  eqger  14667  eqglact  14668  ghminv  14690  conjnmz  14716  subgga  14754  gasubg  14756  galcan  14758  gacan  14759  cntzsubg  14812  cntzmhm  14814  sylow1lem1  14909  sylow2blem2  14932  sylow2blem3  14933  lsmmod  14984  lsmpropd  14986  lsmdisj2  14991  subgdisj1  15000  subgdisj2  15001  efgredleme  15052  efgredlemd  15053  efgredlemc  15054  efgredlem  15056  frgpup3lem  15086  mulgdi  15126  lsm4  15152  cygabl  15177  gsummhm2  15212  gsumpt  15222  gsum2d  15223  dprdfeq0  15257  ablfac1eu  15308  rngcom  15369  isrngd  15375  rnglz  15377  rngrz  15378  rng1eq0  15379  rngmneg1  15382  gsumdixp  15392  unitgrp  15449  irredrmul  15489  drngmul0or  15533  subrginv  15561  subrgunit  15563  srngnvl  15621  srngadd  15622  srngmul  15623  issrngd  15626  lmodvs0  15664  lmodvneg1  15667  lmodvsnegOLD  15668  lmodcom  15671  lmodsubdi  15682  lmodvsinv  15793  lmodvsinv2  15794  lmhmvsca  15802  lvecvs0or  15861  lvecinv  15866  lspsnvs  15867  lspabs2  15873  lspfixed  15881  lspsolv  15896  unitrrg  16034  asclpropd  16085  psrass1lem  16123  psrlidm  16148  psrridm  16149  mvrf1  16170  mplmon2mul  16242  coe1pwmul  16355  prmirredlem  16446  mulgrhm2  16461  chrrhm  16485  znidomb  16515  ip0r  16541  ipdir  16543  ipdi  16544  ipass  16549  ipassr  16550  phlpropd  16559  ocvpj  16617  restin  16897  cncmp  17119  cmpsublem  17126  conndisj  17142  cnconn  17148  kgencmp2  17241  ufldom  17657  tgplacthmeo  17786  ghmcnp  17797  divstgpopn  17802  divstgphaus  17805  tsmsxplem2  17836  xpsdsval  17945  blpnfctr  17982  xmssym  18011  ressxms  18071  isngp2  18119  ngppropd  18153  nminvr  18180  blcvx  18304  icccvx  18448  pcohtpylem  18517  pcohtpy  18518  pjthlem1  18801  ovollb2lem  18847  ovolicc2lem1  18876  ovolicc2lem5  18880  volsup  18913  ovolioo  18925  uniiccdif  18933  uniioombllem3  18940  uniioombllem4  18941  vitalilem3  18965  itg1sub  19064  itg2const  19095  iblcnlem1  19142  itgcnlem  19144  itgaddlem2  19178  itgsub  19180  itgabs  19189  ditgsplit  19211  dvmulbr  19288  dvcmul  19293  dvcmulf  19294  dvrec  19304  dvmptres3  19305  dvmptadd  19309  dvmptmul  19310  dvmptres2  19311  dvmptneg  19315  dvmptsub  19316  dvmptcj  19317  dvmptco  19321  dveflem  19326  dvlip  19340  dvlipcn  19341  dvlip2  19342  dvcvx  19367  dvfsumle  19368  dvfsumabs  19370  dvfsumlem1  19373  dvfsumlem2  19374  ftc2  19391  ftc2ditglem  19392  itgparts  19394  itgsubstlem  19395  itgsubst  19396  evlslem1  19399  evlseu  19400  evlssca  19406  evlsvar  19407  pf1ind  19438  fta1glem1  19551  fta1blem  19554  plyeq0lem  19592  plymullem1  19596  coeeulem  19606  coe0  19637  coesub  19638  dvply1  19664  plydivlem4  19676  plyrem  19685  fta1lem  19687  vieta1  19692  plyexmo  19693  elqaalem2  19700  aareccl  19706  aannenlem1  19708  aaliou3lem2  19723  dvtaylp  19749  taylthlem1  19752  radcnvlem1  19789  pserdvlem2  19804  efcvx  19825  tangtx  19873  efif1olem3  19906  efif1olem4  19907  lognegb  19943  efiarg  19961  cosargd  19962  tanarg  19970  logtayl  20007  cxpsub  20029  cxproot  20037  cxpsqr  20050  cxpcn3lem  20087  cxpaddlelem  20091  abscxpbnd  20093  root1eq1  20095  cxpeq  20097  logrec  20117  isosctrlem2  20119  isosctrlem3  20120  isosctr  20121  ssscongptld  20122  chordthmlem  20129  quad2  20135  dcubic1lem  20139  mcubic  20143  cubic2  20144  cubic  20145  dquartlem2  20148  dquart  20149  quart1lem  20151  quart1  20152  asinlem2  20165  asinlem3  20167  asinsin  20188  sinacos  20201  atanlogsublem  20211  efiatan2  20213  2efiatan  20214  tanatan  20215  atantan  20219  atans2  20227  dvatan  20231  atantayl  20233  atantayl2  20234  log2cnv  20240  rlimcnp2  20261  cxplim  20266  cxp2lim  20271  cvxcl  20279  scvxcvx  20280  wilthlem1  20306  wilthlem2  20307  ftalem5  20314  basellem3  20320  basellem5  20322  basellem8  20325  mumullem2  20418  musum  20431  musumsum  20432  muinv  20433  sgmppw  20436  1sgmprm  20438  1sgm2ppw  20439  ppiub  20443  logfac2  20456  chpchtsum  20458  perfectlem1  20468  perfectlem2  20469  dchrn0  20489  dchrfi  20494  dchrabs  20499  dchrptlem1  20503  dchrhash  20510  dchr2sum  20512  sum2dchr  20513  bposlem6  20528  bposlem9  20531  lgsvalmod  20554  lgsdilem  20561  lgsne0  20572  lgssq  20574  lgssq2  20575  lgsqr  20585  lgsdchrval  20586  lgsdchr  20587  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem4  20591  lgsquadlem1  20593  lgsquadlem3  20595  lgsquad3  20600  m1lgs  20601  rplogsumlem1  20633  rplogsumlem2  20634  dchrisumlem2  20639  dchrisum0fno1  20660  rpvmasum2  20661  dchrisum0lem1  20665  dchrisum0lem2  20667  mudivsum  20679  mulog2sumlem1  20683  vmalogdivsum  20688  2vmadivsumlem  20689  logsqvma  20691  selberglem2  20695  selberg2lem  20699  selberg3lem1  20706  selberg4lem1  20709  selberg4  20710  pntrsumo1  20714  selbergr  20717  selberg34r  20720  pntrlog2bndlem3  20728  pntrlog2bndlem4  20729  pntibndlem2  20740  pntlemg  20747  pntlemr  20751  pntlemf  20754  ostthlem1  20776  padicabvcxp  20781  ostth3  20787  grpoidinvlem1  20871  grpoideu  20876  grporcan  20888  grpolcan  20900  grpoasscan1  20904  grpoinvop  20908  grpopnpcan2  20920  gxsuc  20939  gxsub  20943  gxmul  20945  ablo4  20954  subgoinv  20975  ablomul  21022  ghgrp  21035  ghablo  21036  rngolz  21068  rngorz  21069  nvadd12  21179  nvscom  21187  nvmul0or  21210  nvz0  21234  smcnlem  21270  ipidsq  21286  sspz  21311  lno0  21334  lnoadd  21336  lnomul  21338  ipasslem3  21411  dipdi  21421  dipassr  21424  dipsubdi  21427  ubthlem2  21450  hvmul0or  21604  hvadd12  21614  hvadd4  21615  hvmulcom  21622  normneg  21723  pjhthlem1  21970  chj12  22113  spanunsni  22158  5oalem2  22234  3oalem2  22242  mayete3iOLD  22308  hoadd4  22364  homul12  22385  hosubdi  22388  honegsubdi  22390  hosub4  22393  adj2  22514  lnopmul  22547  lnopaddi  22551  lnfnaddi  22623  lnfnmuli  22624  cnlnadjlem6  22652  adjeq0  22671  leopmul  22714  opsqrlem1  22720  opsqrlem6  22725  hstnmoc  22803  strlem1  22830  chirredlem3  22972  bcm1n  23032  xmulcand  23104  xreceu  23105  xaddeq0  23304  xrsmulgzz  23307  xrge0adddir  23332  esummulc1  23449  measxun2  23538  measssd  23543  totprobd  23629  zetacvg  23689  subfaclim  23719  cvxscon  23774  rescon  23777  cvmliftmolem1  23812  cvmliftlem7  23822  cvmliftlem13  23827  cvmlift2lem7  23840  cvmlift3lem5  23854  ghomf1olem  24001  funsseq  24125  brbtwn2  24533  axsegconlem10  24554  ax5seglem3  24559  ax5seglem6  24562  axpaschlem  24568  axeuclidlem  24590  axcontlem2  24593  axcontlem7  24598  axcontlem8  24599  bpolydiflem  24789  bpoly4  24794  fsumcube  24795  areacirclem2  24925  areacirclem5  24929  areacirc  24931  multinvb  25423  zerdivemp1  25436  mslb1  25607  trnij  25615  addcanrg  25667  idsubfun  25858  clsun  26246  topjoin  26314  cocanfo  26374  ablo4pnp  26570  zerdivemp1x  26586  crngm4  26628  crngohomfo  26631  diophrw  26838  eldioph2lem1  26839  pellexlem2  26915  pellexlem6  26919  pellex  26920  pell1234qrne0  26938  pell1234qrreccl  26939  pell1qrgaplem  26958  rmxm1  27019  oddcomabszz  27029  jm2.19lem1  27082  jm3.1lem2  27111  dnnumch3  27144  pwssplit4  27191  uvcresum  27242  lmimlbs  27306  flcidc  27379  psgnunilem2  27418  psgnghm  27437  gsumcom3  27454  hashgcdlem  27516  deg1mhm  27526  dvsconst  27547  dvsid  27548  expgrowth  27552  itgsinexplem1  27748  sigaradd  27856  cevathlem1  27857  bnj1379  28863  bnj1321  29057  lfl0  29255  lfladd  29256  lflmul  29258  eqlkr3  29291  olm11  29417  latm12  29420  cmtcomlemN  29438  omlspjN  29451  hlatj12  29560  1cvrjat  29664  dalemrotyz  29847  padd12N  30028  pmapjlln1  30044  atmod2i1  30050  pmapocjN  30119  pnonsingN  30122  pexmidN  30158  lhp2at0  30221  lhpelim  30226  ltrncnv  30335  ltrnmw  30340  cdleme7c  30434  cdleme15b  30464  cdlemednpq  30488  cdleme20y  30491  cdleme20m  30512  cdleme22cN  30531  cdleme22d  30532  cdleme23b  30539  cdleme30a  30567  cdleme35h  30645  cdlemeg46frv  30714  cdlemg2fv2  30789  cdlemg2l  30792  cdlemg2m  30793  cdlemg8c  30818  cdlemg10bALTN  30825  cdlemg12  30839  cdlemg13a  30840  cdlemg18c  30869  cdlemg19  30873  trlcoat  30912  cdlemg47  30925  tendo1ne0  31017  cdlemk9  31028  cdlemk9bN  31029  dia2dimlem1  31254  tendolinv  31295  tendorinv  31296  dvhlveclem  31298  doca3N  31317  dihmeetlem7N  31500  dihjatc1  31501  dihmeetlem18N  31514  dochnoncon  31581  dihjatc  31607  dihjatcclem1  31608  dihjatcclem4  31611  dochsnkr  31662  lcfl7lem  31689  lcfl8  31692  lcfl9a  31695  lclkrlem1  31696  lclkrlem2e  31701  lclkrlem2j  31706  lcfrlem1  31732  lcfrlem9  31740  lcfrlem23  31755  lcfrlem31  31763  mapd0  31855  mapdpglem21  31882  baerlem3lem1  31897  baerlem5alem1  31898  mapdindp4  31913  mapdh6gN  31932  hdmap1l6g  32007  hgmapval0  32085  hgmaprnlem1N  32089  hlhilhillem  32153
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator