Theorem 3eqtr3d 2652

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

Step	Hyp	Ref	Expression
1		3eqtr3d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
3	1, 2	eqtr3d 2646	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	eqtr3d 2646	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  mpteqb  6207  fvmptt  6208  fsnunfv  6358  f1ocnvfv1  6432  f1ocnvfv2  6433  fcof1  6442  weniso  6504  caov12d  6753  caov13d  6755  caov411d  6757  caovmo  6769  grprinvlem  6770  grprinvd  6771  grpridd  6772  onovuni  7326  tfrlem5  7363  seqomlem1  7432  seqomlem4  7435  onasuc  7495  onesuc  7497  oeeui  7569  fopwdom  7953  unxpdomlem2  8050  cantnfres  8457  cnfcom2lem  8481  cnfcom2  8482  cardiun  8691  ackbij1lem16  8940  ackbij2lem2  8945  fpwwe2lem6  9336  fpwwe2lem8  9338  canthp1lem2  9354  mul12  10081  mul4  10084  addid1  10095  addcan  10099  addcom  10101  addcomd  10117  add12  10132  ppncan  10202  addsub4  10203  subaddeqd  10325  muladd  10341  mulcand  10539  receu  10551  div13  10585  divdivdiv  10605  divcan5  10606  divdiv1  10615  divdiv2  10616  halfaddsub  11142  xadddi  11997  xov1plusxeqvd  12189  fztp  12267  flzadd  12489  fldiv  12521  mulp1mod1  12573  modnegd  12587  modsub12d  12589  2submod  12593  seqm1  12680  seqcaopr  12700  seqf1o  12704  exprec  12763  expsub  12770  zesq  12849  digit1  12860  discr1  12862  discr  12863  facnn2  12931  faclbnd6  12948  hashfz1  12996  hashdom  13029  hashun  13032  hashbclem  13093  hashfac  13099  seqcoll  13105  ccatopth  13322  repsw2  13541  repsw3  13542  shftval3  13664  crre  13702  resub  13715  imsub  13723  cjsub  13737  abslem2  13927  sqreulem  13947  climshft2  14161  isercolllem2  14244  iseraltlem2  14261  iseraltlem3  14262  fsumsub  14362  telfsumo  14375  telfsumo2  14376  hashiun  14395  bcxmas  14406  climcndslem1  14420  climcndslem2  14421  trireciplem  14433  geoser  14438  geo2sum2  14444  fprodm1  14536  fallfacfwd  14606  binomfallfaclem2  14610  bpolydiflem  14624  bpoly4  14629  fsumcube  14630  sinsub  14737  cossub  14738  rpnnen2lem10  14791  ruclem12  14809  mod2eq1n2dvds  14909  pwp1fsum  14952  divalglem9  14962  bitsinv1lem  15001  bitsinv1  15002  bitsf1  15006  sadasslem  15030  bitsres  15033  smup1  15049  smumul  15053  modgcd  15091  absmulgcd  15104  gcdmultiplez  15108  eucalg  15138  lcmgcd  15158  lcmid  15160  lcmftp  15187  numdensq  15300  dfphi2  15317  phiprm  15320  fermltl  15327  prmdiveq  15329  hashgcdlem  15331  odzdvds  15338  powm2modprm  15346  modprm0  15348  coprimeprodsq  15351  pythagtriplem6  15364  pythagtriplem7  15365  pythagtriplem12  15369  pythagtriplem16  15373  pcaddlem  15430  sumhash  15438  pcfac  15441  pockthlem  15447  prmreclem6  15463  4sqlem12  15498  4sqlem15  15501  vdwlem3  15525  vdwlem6  15528  vdwlem9  15531  ramub1lem2  15569  cshwshashlem2  15641  qusaddvallem  16034  xpsaddlem  16058  xpsvsca  16062  mrcun  16105  homfeqval  16180  comfeqval  16191  sectcan  16238  sectco  16239  sectmon  16265  monsect  16266  funcsect  16355  setcmon  16560  resscatc  16578  catciso  16580  evlfcllem  16684  curf2cl  16694  curfcl  16695  yonedalem4c  16740  yonedalem3b  16742  yonedainv  16744  latj12  16919  mnd12g  17129  resmhm  17182  pwsco2mhm  17194  frmdup3lem  17226  grprcan  17278  grplcan  17300  grpasscan1  17301  grpinv11  17307  grpinvnz  17309  grplmulf1o  17312  grpinvpropd  17313  grpinvadd  17316  grpsubsub4  17331  dfgrp3  17337  imasgrp2  17353  mhmid  17359  mhmmnd  17360  mulgz  17391  mulgdirlem  17395  mulgdir  17396  mulgass  17402  mulgsubdir  17405  mulgpropd  17407  pwsmulg  17410  isnsg3  17451  nmzsubg  17458  ssnmz  17459  eqger  17467  eqglact  17468  ghminv  17490  conjnmz  17517  subgga  17556  gasubg  17558  galcan  17560  gacan  17561  cntzsubg  17592  cntzmhm  17594  psgnunilem2  17738  sylow1lem1  17836  sylow2blem2  17859  sylow2blem3  17860  lsmmod  17911  lsmpropd  17913  lsmdisj2  17918  subgdisj1  17927  subgdisj2  17928  efgredleme  17979  efgredlemd  17980  efgredlemc  17981  efgredlem  17983  frgpup3lem  18013  mulgdi  18055  ghmcmn  18060  lsm4  18086  cygabl  18115  gsummhm2  18162  gsumpt  18184  gsum2d  18194  dprdfeq0  18244  ablfac1eu  18295  ringcom  18402  isringd  18408  ringlz  18410  ringrz  18411  ring1eq0  18413  ringmneg1  18419  gsumdixp  18432  unitgrp  18490  irredrmul  18530  drngmul0or  18591  subrginv  18619  subrgunit  18621  abvrec  18659  srngnvl  18679  srngadd  18680  srngmul  18681  issrngd  18684  lmodvs0  18720  lmodvneg1  18729  lmodcom  18732  lmodsubdi  18743  lmodvsinv  18857  lmodvsinv2  18858  lmhmvsca  18866  lvecvs0or  18929  lvecinv  18934  lspsnvs  18935  lspabs2  18941  lspfixed  18949  lspsolv  18964  unitrrg  19114  asclpropd  19167  psrass1lem  19198  psrlidm  19224  psrridm  19225  mvrf1  19246  mplmon2mul  19322  evlslem1  19336  evlseu  19337  evlssca  19343  evlsvar  19344  coe1pwmul  19470  pf1ind  19540  prmirredlem  19660  mulgrhm2  19666  chrrhm  19698  znidomb  19729  psgnghm  19745  psgninv  19747  zrhpsgnodpm  19757  evpmodpmf1o  19761  psgndiflemB  19765  ip0r  19801  ipdir  19803  ipdi  19804  ipass  19809  ipassr  19810  phlpropd  19819  ocvpj  19880  uvcresum  19951  lmimlbs  19994  gsumcom3  20024  mat0dimbas0  20091  mdetrlin  20227  mdetrsca  20228  mdetr0  20230  mdetunilem8  20244  mdetuni0  20246  mdetmul  20248  maducoeval2  20265  madurid  20269  madulid  20270  matinv  20302  matunit  20303  slesolinv  20305  slesolinvbi  20306  cpmadugsumlemF  20500  restin  20780  cncmp  21005  cmpsublem  21012  conndisj  21029  cnconn  21035  kgencmp2  21159  ufldom  21576  tgplacthmeo  21717  ghmcnp  21728  qustgpopn  21733  qustgphaus  21736  tsmsxplem2  21767  tususp  21886  xpsdsval  21996  blpnfctr  22051  xmssym  22080  ressxms  22140  isngp2  22211  ngppropd  22251  nminvr  22283  blcvx  22409  icccvx  22557  pcohtpylem  22627  pcohtpy  22628  clmvscom  22698  cvsmuleqdivd  22742  cvsdiveqd  22743  pjthlem1  23016  ovollb2lem  23063  ovolicc2lem1  23092  ovolicc2lem5  23096  volsup  23131  ovolioo  23143  uniiccdif  23152  uniioombllem3  23159  uniioombllem4  23160  vitalilem3  23185  itg1sub  23282  itg2const  23313  iblcnlem1  23360  itgcnlem  23362  itgaddlem2  23396  itgsub  23398  itgabs  23407  ditgsplit  23431  dvmulbr  23508  dvcmul  23513  dvcmulf  23514  dvrec  23524  dvmptres3  23525  dvmptadd  23529  dvmptmul  23530  dvmptres2  23531  dvmptneg  23535  dvmptsub  23536  dvmptcj  23537  dvmptco  23541  dveflem  23546  dvlip  23560  dvlipcn  23561  dvlip2  23562  dvcvx  23587  dvfsumle  23588  dvfsumabs  23590  dvfsumlem1  23593  dvfsumlem2  23594  ftc2  23611  ftc2ditglem  23612  itgparts  23614  itgsubstlem  23615  itgsubst  23616  fta1glem1  23729  fta1blem  23732  plyeq0lem  23770  plymullem1  23774  coeeulem  23784  coe0  23816  coesub  23817  dvply1  23843  plydivlem4  23855  plyrem  23864  fta1lem  23866  vieta1  23871  plyexmo  23872  elqaalem2  23879  aareccl  23885  aannenlem1  23887  aaliou3lem2  23902  dvtaylp  23928  taylthlem1  23931  radcnvlem1  23971  pserdvlem2  23986  efcvx  24007  ptolemy  24052  tangtx  24061  efif1olem3  24094  efif1olem4  24095  efabl  24100  lognegb  24140  efiarg  24157  cosargd  24158  tanarg  24169  logtayl  24206  cxpneg  24227  cxpsub  24228  cxprec  24232  cxproot  24236  cxpsqrt  24249  cxpcn3lem  24288  cxpaddlelem  24292  abscxpbnd  24294  root1eq1  24296  cxpeq  24298  logrec  24301  isosctrlem2  24349  isosctrlem3  24350  isosctr  24351  ssscongptld  24352  chordthmlem  24359  heron  24365  quad2  24366  dcubic1lem  24370  mcubic  24374  cubic2  24375  cubic  24376  dquartlem2  24379  dquart  24380  quart1lem  24382  quart1  24383  asinlem2  24396  asinlem3  24398  asinsin  24419  sinacos  24432  atanlogsublem  24442  efiatan2  24444  2efiatan  24445  tanatan  24446  atantan  24450  atans2  24458  dvatan  24462  atantayl  24464  atantayl2  24465  log2cnv  24471  rlimcnp2  24493  cxplim  24498  cxp2lim  24503  cvxcl  24511  scvxcvx  24512  zetacvg  24541  lgamgulmlem4  24558  lgamcvg2  24581  gamp1  24584  wilthlem1  24594  wilthlem2  24595  ftalem5  24603  basellem3  24609  basellem5  24611  basellem8  24614  mumullem2  24706  musum  24717  musumsum  24718  muinv  24719  sgmppw  24722  1sgmprm  24724  1sgm2ppw  24725  ppiub  24729  logfac2  24742  chpchtsum  24744  perfectlem1  24754  perfectlem2  24755  dchrn0  24775  dchrfi  24780  dchrabs  24785  dchrptlem1  24789  dchrhash  24796  dchr2sum  24798  sum2dchr  24799  bposlem6  24814  bposlem9  24817  lgsvalmod  24841  lgsdilem  24849  lgsne0  24860  lgssq  24862  lgssq2  24863  lgsqr  24876  lgsdchrval  24879  lgsdchr  24880  gausslemma2dlem6  24897  gausslemma2d  24899  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem4  24903  lgsquadlem1  24905  lgsquadlem3  24907  lgsquad3  24912  m1lgs  24913  rplogsumlem1  24973  rplogsumlem2  24974  dchrisumlem2  24979  dchrisum0fno1  25000  rpvmasum2  25001  dchrisum0lem1  25005  dchrisum0lem2  25007  mudivsum  25019  mulog2sumlem1  25023  vmalogdivsum  25028  2vmadivsumlem  25029  logsqvma  25031  selberglem2  25035  selberg2lem  25039  selberg3lem1  25046  selberg4lem1  25049  selberg4  25050  pntrsumo1  25054  selbergr  25057  selberg34r  25060  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntibndlem2  25080  pntlemg  25087  pntlemr  25091  pntlemf  25094  ostthlem1  25116  padicabvcxp  25121  ostth3  25127  tgcgrcomlr  25175  tgifscgr  25203  iscgrglt  25209  tgbtwnconn1lem2  25268  tgbtwnconn1lem3  25269  mirne  25362  miduniq2  25382  krippenlem  25385  ragcgr  25402  cgrg3col4  25534  f1otrg  25551  ttgcontlem1  25565  brbtwn2  25585  axsegconlem10  25606  ax5seglem3  25611  ax5seglem6  25614  axpaschlem  25620  axeuclidlem  25642  axcontlem2  25645  axcontlem7  25650  axcontlem8  25651  cusgrasizeindslem2  26003  frgrancvvdeq  26569  frgrancvvdgeq  26570  numclwwlk7  26641  grpoidinvlem1  26742  grpoideu  26747  grporcan  26756  grpolcan  26768  grpoinvop  26771  ablo4  26788  nvscom  26868  nvmul0or  26889  nvz0  26907  smcnlem  26936  ipidsq  26949  sspz  26974  lno0  26995  lnoadd  26997  lnomul  26999  ipasslem3  27072  dipdi  27082  dipassr  27085  dipsubdi  27088  ubthlem2  27111  hvmul0or  27266  hvadd12  27276  hvadd4  27277  hvmulcom  27284  normneg  27385  pjhthlem1  27634  chj12  27777  spanunsni  27822  5oalem2  27898  3oalem2  27906  hoadd4  28027  homul12  28048  hosubdi  28051  honegsubdi  28053  hosub4  28056  adj2  28177  lnopmul  28210  lnopaddi  28214  lnfnaddi  28286  lnfnmuli  28287  cnlnadjlem6  28315  adjeq0  28334  leopmul  28377  opsqrlem1  28383  opsqrlem6  28388  hstnmoc  28466  strlem1  28493  chirredlem3  28635  fpwrelmapffslem  28895  subeqxfrd  28899  xaddeq0  28907  bcm1n  28941  divnumden2  28951  xmulcand  28960  xreceu  28961  bhmafibid1  28975  2sqmod  28979  xrsmulgzz  29009  xrge0adddir  29023  xrge0adddi  29024  abliso  29027  ogrpaddltrbid  29052  ogrpinvlt  29055  archiabllem1a  29076  archiabllem1  29078  archiabllem2c  29080  slmdvs0  29109  dvrcan5  29124  ornglmullt  29138  orngrmullt  29139  rhmunitinv  29153  mdetpmtr2  29218  madjusmdetlem1  29221  mdetlap  29226  qtophaus  29231  qqhval2lem  29353  esumpad  29444  esummulc1  29470  esumsup  29478  measxun2  29600  measssd  29605  inelcarsg  29700  carsggect  29707  carsgclctunlem2  29708  pmeasmono  29713  oddpwdc  29743  eulerpartlemgs2  29769  eulerpartlemn  29770  totprobd  29815  signstfvn  29972  signstfveq0  29980  bnj1379  30155  bnj1321  30349  subfaclim  30424  cvxscon  30479  rescon  30482  cvmliftmolem1  30517  cvmliftlem7  30527  cvmliftlem13  30532  cvmlift2lem7  30545  cvmlift3lem5  30559  elmsta  30699  msubff1  30707  mthmpps  30733  bcm1nt  30876  faclim2  30887  funsseq  30912  clsun  31493  topjoin  31530  bj-bary1lem  32337  finxpreclem4  32407  matunitlindflem1  32575  ptrest  32578  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem9  32588  poimirlem11  32590  poimirlem12  32591  poimirlem26  32605  poimirlem27  32606  itg2addnclem  32631  itg2addnclem3  32633  itgaddnclem2  32639  itgsubnc  32642  iblmulc2nc  32645  itgabsnc  32649  ftc2nc  32664  areacirclem1  32670  areacirclem4  32673  areacirc  32675  cocanfo  32682  ablo4pnp  32849  rngolz  32891  rngorz  32892  zerdivemp1x  32916  crngm4  32972  crngohomfo  32975  fsumshftdOLD  33256  lfl0  33370  lfladd  33371  lflmul  33373  eqlkr3  33406  olm11  33532  latm12  33535  cmtcomlemN  33553  omlspjN  33566  hlatj12  33675  1cvrjat  33779  dalemrotyz  33962  padd12N  34143  pmapjlln1  34159  atmod2i1  34165  pmapocjN  34234  pnonsingN  34237  pexmidN  34273  lhp2at0  34336  lhpelim  34341  ltrncnv  34450  ltrnmwOLD  34456  cdleme7c  34550  cdleme15b  34580  cdlemednpq  34604  cdleme20yOLD  34608  cdleme20m  34629  cdleme22cN  34648  cdleme22d  34649  cdleme23b  34656  cdleme30a  34684  cdleme35h  34762  cdlemeg46frv  34831  cdlemg2fv2  34906  cdlemg2l  34909  cdlemg2m  34910  cdlemg8c  34935  cdlemg10bALTN  34942  cdlemg12  34956  cdlemg13a  34957  cdlemg18c  34986  cdlemg19  34990  trlcoat  35029  cdlemg47  35042  tendo1ne0  35134  cdlemk9  35145  cdlemk9bN  35146  dia2dimlem1  35371  tendolinv  35412  tendorinv  35413  dvhlveclem  35415  doca3N  35434  dihmeetlem7N  35617  dihjatc1  35618  dihmeetlem18N  35631  dochnoncon  35698  dihjatc  35724  dihjatcclem1  35725  dihjatcclem4  35728  dochsnkr  35779  lcfl7lem  35806  lcfl8  35809  lcfl9a  35812  lclkrlem1  35813  lclkrlem2e  35818  lclkrlem2j  35823  lcfrlem1  35849  lcfrlem9  35857  lcfrlem23  35872  lcfrlem31  35880  mapd0  35972  mapdpglem21  35999  baerlem3lem1  36014  baerlem5alem1  36015  mapdindp4  36030  mapdh6gN  36049  hdmap1l6g  36124  hgmapval0  36202  hgmaprnlem1N  36206  hlhilhillem  36270  diophrw  36340  eldioph2lem1  36341  pellexlem2  36412  pellexlem6  36416  pellex  36417  pell1234qrne0  36435  pell1234qrreccl  36436  pell1qrgaplem  36455  rmxm1  36517  oddcomabszz  36527  jm2.19lem1  36574  jm3.1lem2  36603  dnnumch3  36635  pwssplit4  36677  flcidc  36763  deg1mhm  36804  itgpowd  36819  radcnvrat  37535  nzprmdif  37540  hashnzfz  37541  dvsconst  37551  dvsid  37552  expgrowth  37556  bccm1k  37563  bccn1  37565  binomcxplemnotnn0  37577  subadd4b  38435  sumnnodd  38697  icccncfext  38773  dvresntr  38806  itgsinexplem1  38845  itgsinexp  38846  stoweidlem1  38894  wallispi2lem2  38965  stirlinglem3  38969  stirlinglem5  38971  stirlinglem10  38976  stirlinglem15  38981  dirkertrigeqlem3  38993  dirkercncflem2  38997  fourierdlem26  39026  fourierdlem42  39042  fourierdlem66  39065  fourierdlem73  39072  fourierdlem81  39080  fourierdlem83  39082  fourierdlem107  39106  etransclem23  39150  meaiininclem  39376  vonvolmbl  39551  iccvonmbllem  39569  sigaradd  39704  cevathlem1  39705  m1mod0mod1  39949  fmtnorec3  39998  proththd  40069  perfectALTVlem1  40164  perfectALTVlem2  40165  imarnf1pr  40326  cusgrsizeindslem  40667  frgrncvvdeq  41480  av-numclwwlk7  41545  rnglz  41674  pw2m1lepw2m1  42104  nnpw2pmod  42175  dignn0flhalflem1  42207  aacllem  42356  amgmlemALT  42358  young2d  42360