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

Theorem 3eqtr3d 2651
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 (𝜑𝐴 = 𝐵)
3eqtr3d.2 (𝜑𝐴 = 𝐶)
3eqtr3d.3 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
3eqtr3d (𝜑𝐶 = 𝐷)

Proof of Theorem 3eqtr3d
StepHypRef Expression
1 3eqtr3d.1 . . 3 (𝜑𝐴 = 𝐵)
2 3eqtr3d.2 . . 3 (𝜑𝐴 = 𝐶)
31, 2eqtr3d 2645 . 2 (𝜑𝐵 = 𝐶)
4 3eqtr3d.3 . 2 (𝜑𝐵 = 𝐷)
53, 4eqtr3d 2645 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602
This theorem is referenced by:  mpteqb  6192  fvmptt  6193  fsnunfv  6336  f1ocnvfv1  6410  f1ocnvfv2  6411  fcof1  6420  weniso  6482  caov12d  6730  caov13d  6732  caov411d  6734  caovmo  6746  grprinvlem  6747  grprinvd  6748  grpridd  6749  onovuni  7303  tfrlem5  7340  seqomlem1  7409  seqomlem4  7412  onasuc  7472  onesuc  7474  oeeui  7546  fopwdom  7930  unxpdomlem2  8027  cantnfres  8434  cnfcom2lem  8458  cnfcom2  8459  cardiun  8668  ackbij1lem16  8917  ackbij2lem2  8922  fpwwe2lem6  9313  fpwwe2lem8  9315  canthp1lem2  9331  mul12  10053  mul4  10056  addid1  10067  addcan  10071  addcom  10073  addcomd  10089  add12  10104  ppncan  10174  addsub4  10175  subaddeqd  10297  muladd  10313  mulcand  10509  receu  10521  div13  10555  divdivdiv  10575  divcan5  10576  divdiv1  10585  divdiv2  10586  halfaddsub  11112  xadddi  11954  xov1plusxeqvd  12145  fztp  12222  flzadd  12444  fldiv  12476  mulp1mod1  12528  modnegd  12542  modsub12d  12544  2submod  12548  seqm1  12635  seqcaopr  12655  seqf1o  12659  exprec  12718  expsub  12725  zesq  12804  digit1  12815  discr1  12817  discr  12818  facnn2  12886  faclbnd6  12903  hashfz1  12948  hashdom  12981  hashun  12984  hashbclem  13045  hashfac  13051  seqcoll  13057  ccatopth  13268  repsw2  13487  repsw3  13488  shftval3  13610  crre  13648  resub  13661  imsub  13669  cjsub  13683  abslem2  13873  sqreulem  13893  climshft2  14107  isercolllem2  14190  iseraltlem2  14207  iseraltlem3  14208  fsumsub  14308  telfsumo  14321  telfsumo2  14322  hashiun  14341  bcxmas  14352  climcndslem1  14366  climcndslem2  14367  trireciplem  14379  geoser  14384  geo2sum2  14390  fprodm1  14482  fallfacfwd  14552  binomfallfaclem2  14556  bpolydiflem  14570  bpoly4  14575  fsumcube  14576  sinsub  14683  cossub  14684  rpnnen2lem10  14737  ruclem12  14755  mod2eq1n2dvds  14855  pwp1fsum  14898  divalglem9  14908  bitsinv1lem  14947  bitsinv1  14948  bitsf1  14952  sadasslem  14976  bitsres  14979  smup1  14995  smumul  14999  modgcd  15037  absmulgcd  15050  gcdmultiplez  15054  eucalg  15084  lcmgcd  15104  lcmid  15106  lcmftp  15133  numdensq  15246  dfphi2  15263  phiprm  15266  fermltl  15273  prmdiveq  15275  hashgcdlem  15277  odzdvds  15284  powm2modprm  15292  modprm0  15294  coprimeprodsq  15297  pythagtriplem6  15310  pythagtriplem7  15311  pythagtriplem12  15315  pythagtriplem16  15319  pcaddlem  15376  sumhash  15384  pcfac  15387  pockthlem  15393  prmreclem6  15409  4sqlem12  15444  4sqlem15  15447  vdwlem3  15471  vdwlem6  15474  vdwlem9  15477  ramub1lem2  15515  cshwshashlem2  15587  qusaddvallem  15980  xpsaddlem  16004  xpsvsca  16008  mrcun  16051  homfeqval  16126  comfeqval  16137  sectcan  16184  sectco  16185  sectmon  16211  monsect  16212  funcsect  16301  setcmon  16506  resscatc  16524  catciso  16526  evlfcllem  16630  curf2cl  16640  curfcl  16641  yonedalem4c  16686  yonedalem3b  16688  yonedainv  16690  latj12  16865  mnd12g  17075  resmhm  17128  pwsco2mhm  17140  frmdup3lem  17172  grprcan  17224  grplcan  17246  grpasscan1  17247  grpinv11  17253  grpinvnz  17255  grplmulf1o  17258  grpinvpropd  17259  grpinvadd  17262  grpsubsub4  17277  dfgrp3  17283  imasgrp2  17299  mhmid  17305  mhmmnd  17306  mulgz  17337  mulgdirlem  17341  mulgdir  17342  mulgass  17348  mulgsubdir  17351  mulgpropd  17353  pwsmulg  17356  isnsg3  17397  nmzsubg  17404  ssnmz  17405  eqger  17413  eqglact  17414  ghminv  17436  conjnmz  17463  subgga  17502  gasubg  17504  galcan  17506  gacan  17507  cntzsubg  17538  cntzmhm  17540  psgnunilem2  17684  sylow1lem1  17782  sylow2blem2  17805  sylow2blem3  17806  lsmmod  17857  lsmpropd  17859  lsmdisj2  17864  subgdisj1  17873  subgdisj2  17874  efgredleme  17925  efgredlemd  17926  efgredlemc  17927  efgredlem  17929  frgpup3lem  17959  mulgdi  18001  ghmcmn  18006  lsm4  18032  cygabl  18061  gsummhm2  18108  gsumpt  18130  gsum2d  18140  dprdfeq0  18190  ablfac1eu  18241  ringcom  18348  isringd  18354  ringlz  18356  ringrz  18357  ring1eq0  18359  ringmneg1  18365  gsumdixp  18378  unitgrp  18436  irredrmul  18476  drngmul0or  18537  subrginv  18565  subrgunit  18567  abvrec  18605  srngnvl  18625  srngadd  18626  srngmul  18627  issrngd  18630  lmodvs0  18666  lmodvneg1  18675  lmodcom  18678  lmodsubdi  18689  lmodvsinv  18803  lmodvsinv2  18804  lmhmvsca  18812  lvecvs0or  18875  lvecinv  18880  lspsnvs  18881  lspabs2  18887  lspfixed  18895  lspsolv  18910  unitrrg  19060  asclpropd  19113  psrass1lem  19144  psrlidm  19170  psrridm  19171  mvrf1  19192  mplmon2mul  19268  evlslem1  19282  evlseu  19283  evlssca  19289  evlsvar  19290  coe1pwmul  19416  pf1ind  19486  prmirredlem  19605  mulgrhm2  19611  chrrhm  19643  znidomb  19674  psgnghm  19690  psgninv  19692  zrhpsgnodpm  19702  evpmodpmf1o  19706  psgndiflemB  19710  ip0r  19746  ipdir  19748  ipdi  19749  ipass  19754  ipassr  19755  phlpropd  19764  ocvpj  19822  uvcresum  19893  lmimlbs  19936  gsumcom3  19966  mat0dimbas0  20033  mdetrlin  20169  mdetrsca  20170  mdetr0  20172  mdetunilem8  20186  mdetuni0  20188  mdetmul  20190  maducoeval2  20207  madurid  20211  madulid  20212  matinv  20244  matunit  20245  slesolinv  20247  slesolinvbi  20248  cpmadugsumlemF  20442  restin  20722  cncmp  20947  cmpsublem  20954  conndisj  20971  cnconn  20977  kgencmp2  21101  ufldom  21518  tgplacthmeo  21659  ghmcnp  21670  qustgpopn  21675  qustgphaus  21678  tsmsxplem2  21709  tususp  21828  xpsdsval  21937  blpnfctr  21992  xmssym  22021  ressxms  22081  isngp2  22152  ngppropd  22189  nminvr  22216  blcvx  22341  icccvx  22488  pcohtpylem  22558  pcohtpy  22559  clmvscom  22629  cvsmuleqdivd  22671  cvsdiveqd  22672  pjthlem1  22933  ovollb2lem  22980  ovolicc2lem1  23009  ovolicc2lem5  23013  volsup  23048  ovolioo  23060  uniiccdif  23069  uniioombllem3  23076  uniioombllem4  23077  vitalilem3  23102  itg1sub  23199  itg2const  23230  iblcnlem1  23277  itgcnlem  23279  itgaddlem2  23313  itgsub  23315  itgabs  23324  ditgsplit  23348  dvmulbr  23425  dvcmul  23430  dvcmulf  23431  dvrec  23441  dvmptres3  23442  dvmptadd  23446  dvmptmul  23447  dvmptres2  23448  dvmptneg  23452  dvmptsub  23453  dvmptcj  23454  dvmptco  23458  dveflem  23463  dvlip  23477  dvlipcn  23478  dvlip2  23479  dvcvx  23504  dvfsumle  23505  dvfsumabs  23507  dvfsumlem1  23510  dvfsumlem2  23511  ftc2  23528  ftc2ditglem  23529  itgparts  23531  itgsubstlem  23532  itgsubst  23533  fta1glem1  23646  fta1blem  23649  plyeq0lem  23687  plymullem1  23691  coeeulem  23701  coe0  23733  coesub  23734  dvply1  23760  plydivlem4  23772  plyrem  23781  fta1lem  23783  vieta1  23788  plyexmo  23789  elqaalem2  23796  aareccl  23802  aannenlem1  23804  aaliou3lem2  23819  dvtaylp  23845  taylthlem1  23848  radcnvlem1  23888  pserdvlem2  23903  efcvx  23924  ptolemy  23969  tangtx  23978  efif1olem3  24011  efif1olem4  24012  efabl  24017  lognegb  24057  efiarg  24074  cosargd  24075  tanarg  24086  logtayl  24123  cxpneg  24144  cxpsub  24145  cxprec  24149  cxproot  24153  cxpsqrt  24166  cxpcn3lem  24205  cxpaddlelem  24209  abscxpbnd  24211  root1eq1  24213  cxpeq  24215  logrec  24218  isosctrlem2  24266  isosctrlem3  24267  isosctr  24268  ssscongptld  24269  chordthmlem  24276  heron  24282  quad2  24283  dcubic1lem  24287  mcubic  24291  cubic2  24292  cubic  24293  dquartlem2  24296  dquart  24297  quart1lem  24299  quart1  24300  asinlem2  24313  asinlem3  24315  asinsin  24336  sinacos  24349  atanlogsublem  24359  efiatan2  24361  2efiatan  24362  tanatan  24363  atantan  24367  atans2  24375  dvatan  24379  atantayl  24381  atantayl2  24382  log2cnv  24388  rlimcnp2  24410  cxplim  24415  cxp2lim  24420  cvxcl  24428  scvxcvx  24429  zetacvg  24458  lgamgulmlem4  24475  lgamcvg2  24498  gamp1  24501  wilthlem1  24511  wilthlem2  24512  ftalem5  24520  basellem3  24526  basellem5  24528  basellem8  24531  mumullem2  24623  musum  24634  musumsum  24635  muinv  24636  sgmppw  24639  1sgmprm  24641  1sgm2ppw  24642  ppiub  24646  logfac2  24659  chpchtsum  24661  perfectlem1  24671  perfectlem2  24672  dchrn0  24692  dchrfi  24697  dchrabs  24702  dchrptlem1  24706  dchrhash  24713  dchr2sum  24715  sum2dchr  24716  bposlem6  24731  bposlem9  24734  lgsvalmod  24758  lgsdilem  24766  lgsne0  24777  lgssq  24779  lgssq2  24780  lgsqr  24793  lgsdchrval  24796  lgsdchr  24797  gausslemma2dlem6  24814  gausslemma2d  24816  lgseisenlem1  24817  lgseisenlem2  24818  lgseisenlem4  24820  lgsquadlem1  24822  lgsquadlem3  24824  lgsquad3  24829  m1lgs  24830  rplogsumlem1  24890  rplogsumlem2  24891  dchrisumlem2  24896  dchrisum0fno1  24917  rpvmasum2  24918  dchrisum0lem1  24922  dchrisum0lem2  24924  mudivsum  24936  mulog2sumlem1  24940  vmalogdivsum  24945  2vmadivsumlem  24946  logsqvma  24948  selberglem2  24952  selberg2lem  24956  selberg3lem1  24963  selberg4lem1  24966  selberg4  24967  pntrsumo1  24971  selbergr  24974  selberg34r  24977  pntrlog2bndlem3  24985  pntrlog2bndlem4  24986  pntibndlem2  24997  pntlemg  25004  pntlemr  25008  pntlemf  25011  ostthlem1  25033  padicabvcxp  25038  ostth3  25044  tgcgrcomlr  25092  tgifscgr  25121  iscgrglt  25127  tgbtwnconn1lem2  25186  tgbtwnconn1lem3  25187  mirne  25280  miduniq2  25300  krippenlem  25303  ragcgr  25320  cgrg3col4  25452  f1otrg  25469  ttgcontlem1  25483  brbtwn2  25503  axsegconlem10  25524  ax5seglem3  25529  ax5seglem6  25532  axpaschlem  25538  axeuclidlem  25560  axcontlem2  25563  axcontlem7  25568  axcontlem8  25569  cusgrasizeindslem2  25769  frgrancvvdeq  26335  frgrancvvdgeq  26336  numclwwlk7  26407  grpoidinvlem1  26508  grpoideu  26513  grporcan  26522  grpolcan  26534  grpoinvop  26537  grpopnpcan2  26548  ablo4  26557  nvadd12  26646  nvscom  26654  nvmul0or  26677  nvz0  26701  smcnlem  26737  ipidsq  26753  sspz  26778  lno0  26801  lnoadd  26803  lnomul  26805  ipasslem3  26878  dipdi  26888  dipassr  26891  dipsubdi  26894  ubthlem2  26917  hvmul0or  27072  hvadd12  27082  hvadd4  27083  hvmulcom  27090  normneg  27191  pjhthlem1  27440  chj12  27583  spanunsni  27628  5oalem2  27704  3oalem2  27712  hoadd4  27833  homul12  27854  hosubdi  27857  honegsubdi  27859  hosub4  27862  adj2  27983  lnopmul  28016  lnopaddi  28020  lnfnaddi  28092  lnfnmuli  28093  cnlnadjlem6  28121  adjeq0  28140  leopmul  28183  opsqrlem1  28189  opsqrlem6  28194  hstnmoc  28272  strlem1  28299  chirredlem3  28441  fpwrelmapffslem  28701  subeqxfrd  28705  xaddeq0  28713  bcm1n  28747  divnumden2  28757  xmulcand  28766  xreceu  28767  bhmafibid1  28781  2sqmod  28785  xrsmulgzz  28815  xrge0adddir  28829  xrge0adddi  28830  abliso  28833  ogrpaddltrbid  28858  ogrpinvlt  28861  archiabllem1a  28882  archiabllem1  28884  archiabllem2c  28886  slmdvs0  28915  dvrcan5  28930  ornglmullt  28944  orngrmullt  28945  rhmunitinv  28959  mdetpmtr2  29024  madjusmdetlem1  29027  mdetlap  29032  qtophaus  29037  qqhval2lem  29159  esumpad  29250  esummulc1  29276  esumsup  29284  measxun2  29406  measssd  29411  inelcarsg  29506  carsggect  29513  carsgclctunlem2  29514  pmeasmono  29519  oddpwdc  29549  eulerpartlemgs2  29575  eulerpartlemn  29576  totprobd  29621  signstfvn  29778  signstfveq0  29786  bnj1379  29961  bnj1321  30155  subfaclim  30230  cvxscon  30285  rescon  30288  cvmliftmolem1  30323  cvmliftlem7  30333  cvmliftlem13  30338  cvmlift2lem7  30351  cvmlift3lem5  30365  elmsta  30505  msubff1  30513  mthmpps  30539  bcm1nt  30682  faclim2  30693  funsseq  30718  clsun  31299  topjoin  31336  bj-bary1lem  32133  finxpreclem4  32203  matunitlindflem1  32371  ptrest  32374  poimirlem4  32379  poimirlem6  32381  poimirlem7  32382  poimirlem9  32384  poimirlem11  32386  poimirlem12  32387  poimirlem26  32401  poimirlem27  32402  itg2addnclem  32427  itg2addnclem3  32429  itgaddnclem2  32435  itgsubnc  32438  iblmulc2nc  32441  itgabsnc  32445  ftc2nc  32460  areacirclem1  32466  areacirclem4  32469  areacirc  32471  cocanfo  32478  ablo4pnp  32645  rngolz  32687  rngorz  32688  zerdivemp1x  32712  crngm4  32768  crngohomfo  32771  fsumshftdOLD  33052  lfl0  33166  lfladd  33167  lflmul  33169  eqlkr3  33202  olm11  33328  latm12  33331  cmtcomlemN  33349  omlspjN  33362  hlatj12  33471  1cvrjat  33575  dalemrotyz  33758  padd12N  33939  pmapjlln1  33955  atmod2i1  33961  pmapocjN  34030  pnonsingN  34033  pexmidN  34069  lhp2at0  34132  lhpelim  34137  ltrncnv  34246  ltrnmwOLD  34252  cdleme7c  34346  cdleme15b  34376  cdlemednpq  34400  cdleme20yOLD  34404  cdleme20m  34425  cdleme22cN  34444  cdleme22d  34445  cdleme23b  34452  cdleme30a  34480  cdleme35h  34558  cdlemeg46frv  34627  cdlemg2fv2  34702  cdlemg2l  34705  cdlemg2m  34706  cdlemg8c  34731  cdlemg10bALTN  34738  cdlemg12  34752  cdlemg13a  34753  cdlemg18c  34782  cdlemg19  34786  trlcoat  34825  cdlemg47  34838  tendo1ne0  34930  cdlemk9  34941  cdlemk9bN  34942  dia2dimlem1  35167  tendolinv  35208  tendorinv  35209  dvhlveclem  35211  doca3N  35230  dihmeetlem7N  35413  dihjatc1  35414  dihmeetlem18N  35427  dochnoncon  35494  dihjatc  35520  dihjatcclem1  35521  dihjatcclem4  35524  dochsnkr  35575  lcfl7lem  35602  lcfl8  35605  lcfl9a  35608  lclkrlem1  35609  lclkrlem2e  35614  lclkrlem2j  35619  lcfrlem1  35645  lcfrlem9  35653  lcfrlem23  35668  lcfrlem31  35676  mapd0  35768  mapdpglem21  35795  baerlem3lem1  35810  baerlem5alem1  35811  mapdindp4  35826  mapdh6gN  35845  hdmap1l6g  35920  hgmapval0  35998  hgmaprnlem1N  36002  hlhilhillem  36066  diophrw  36136  eldioph2lem1  36137  pellexlem2  36208  pellexlem6  36212  pellex  36213  pell1234qrne0  36231  pell1234qrreccl  36232  pell1qrgaplem  36251  rmxm1  36313  oddcomabszz  36323  jm2.19lem1  36370  jm3.1lem2  36399  dnnumch3  36431  pwssplit4  36473  flcidc  36559  deg1mhm  36600  itgpowd  36615  radcnvrat  37331  nzprmdif  37336  hashnzfz  37337  dvsconst  37347  dvsid  37348  expgrowth  37352  bccm1k  37359  bccn1  37361  binomcxplemnotnn0  37373  subadd4b  38231  sumnnodd  38494  icccncfext  38570  dvresntr  38603  itgsinexplem1  38642  itgsinexp  38643  stoweidlem1  38691  wallispi2lem2  38762  stirlinglem3  38766  stirlinglem5  38768  stirlinglem10  38773  stirlinglem15  38778  dirkertrigeqlem3  38790  dirkercncflem2  38794  fourierdlem26  38823  fourierdlem42  38839  fourierdlem66  38862  fourierdlem73  38869  fourierdlem81  38877  fourierdlem83  38879  fourierdlem107  38903  etransclem23  38947  meaiininclem  39173  vonvolmbl  39348  iccvonmbllem  39366  sigaradd  39501  cevathlem1  39502  m1mod0mod1  39747  fmtnorec3  39796  proththd  39867  perfectALTVlem1  39962  perfectALTVlem2  39963  imarnf1pr  40135  cusgrsizeindslem  40662  frgrncvvdeq  41475  av-numclwwlk7  41540  rnglz  41669  pw2m1lepw2m1  42099  nnpw2pmod  42170  dignn0flhalflem1  42202  aacllem  42312  amgmlemALT  42314  young2d  42316
  Copyright terms: Public domain W3C validator