Theorem 3eqtr3d 2787

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 2781	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	eqtr3d 2781	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  mpteqb  6903  fvmptt  6904  fvsnun2  7064  fsnunfv  7068  f1ocnvfv1  7157  f1ocnvfv2  7158  fcof1  7168  f1ofvswap  7187  weniso  7234  caov12d  7502  caov13d  7504  caov411d  7506  caovmo  7518  onovuni  8182  tfrlem5  8220  seqomlem1  8290  seqomlem4  8293  onasuc  8367  onesuc  8369  oeeui  8442  fopwdom  8876  unxpdomlem2  9037  cantnfres  9444  cnfcom2lem  9468  cnfcom2  9469  updjud  9701  cardiun  9749  ackbij1lem16  10000  ackbij2lem2  10005  fpwwe2lem5  10400  fpwwe2lem7  10402  canthp1lem2  10418  mul12  11149  mul4  11152  addid1  11164  addcan  11168  addcom  11170  addcomd  11186  add12  11201  ppncan  11272  addsub4  11273  subeqxfrd  11393  subaddeqd  11399  muladd  11416  mulcand  11617  receu  11629  div13  11663  divdivdiv  11685  divcan5  11686  divdiv1  11695  divdiv2  11696  halfaddsub  12215  xadddi  13038  xov1plusxeqvd  13239  fztp  13321  flzadd  13555  fldiv  13589  mulp1mod1  13641  modnegd  13655  modsub12d  13657  2submod  13661  seqm1  13749  seqcaopr  13769  seqf1o  13773  exprec  13833  expsub  13840  zesq  13950  digit1  13961  discr1  13963  discr  13964  facnn2  14005  faclbnd6  14022  hashfz1  14069  hashdom  14103  hashun  14106  hashbclem  14173  hashfac  14181  seqcoll  14187  ccatopth  14438  repsw2  14672  repsw3  14673  shftval3  14796  crre  14834  resub  14847  imsub  14855  cjsub  14869  nn0sqeq1  14997  abslem2  15060  sqreulem  15080  bhmafibid1  15186  climshft2  15300  isercolllem2  15386  iseraltlem2  15403  iseraltlem3  15404  fsumsub  15509  telfsumo  15523  telfsumo2  15524  hashiun  15543  bcxmas  15556  climcndslem1  15570  climcndslem2  15571  trireciplem  15583  geoser  15588  geo2sum2  15595  fprodm1  15686  fallfacfwd  15755  binomfallfaclem2  15759  bpolydiflem  15773  bpoly4  15778  fsumcube  15779  sinsub  15886  cossub  15887  rpnnen2lem10  15941  ruclem12  15959  p1modz1  15979  mod2eq1n2dvds  16065  pwp1fsum  16109  divalglem9  16119  bitsinv1lem  16157  bitsinv1  16158  bitsf1  16162  sadasslem  16186  bitsres  16189  smup1  16205  smumul  16209  modgcd  16249  absmulgcd  16266  gcdmultiplezOLD  16270  eucalg  16301  lcmgcd  16321  lcmid  16323  lcmftp  16350  numdensq  16467  dfphi2  16484  phiprm  16487  fermltl  16494  prmdiveq  16496  hashgcdlem  16498  odzdvds  16505  powm2modprm  16513  modprm0  16515  coprimeprodsq  16518  pythagtriplem6  16531  pythagtriplem7  16532  pythagtriplem12  16536  pythagtriplem16  16540  pcaddlem  16598  sumhash  16606  pcfac  16609  pockthlem  16615  prmreclem6  16631  4sqlem12  16666  4sqlem15  16669  vdwlem3  16693  vdwlem6  16696  vdwlem9  16699  ramub1lem2  16737  cshwshashlem2  16807  qusaddvallem  17271  xpsaddlem  17293  xpsvsca  17297  mrcun  17340  homfeqval  17415  comfeqval  17426  sectcan  17476  sectco  17477  sectmon  17503  monsect  17504  funcsect  17596  setcmon  17811  resscatc  17833  catciso  17835  evlfcllem  17948  curf2cl  17958  curfcl  17959  yonedalem4c  18004  yonedalem3b  18006  yonedainv  18008  latj12  18211  grprinvlem  18366  grprinvd  18367  grpridd  18368  mnd12g  18407  resmhm  18468  pwsco2mhm  18480  frmdup3lem  18514  grprcan  18622  grplcan  18646  grpasscan1  18647  grpinv11  18653  grpinvnz  18655  grplmulf1o  18658  grpinvpropd  18659  grpinvadd  18662  grpsubsub4  18677  dfgrp3  18683  imasgrp2  18699  mhmid  18705  mhmmnd  18706  mulgz  18740  mulgdirlem  18743  mulgdir  18744  mulgass  18749  mulgsubdir  18752  mulgpropd  18754  pwsmulg  18757  isnsg3  18797  nmzsubg  18802  ssnmz  18803  eqger  18815  eqglact  18816  cyccom  18831  ghminv  18850  conjnmz  18877  subgga  18915  gasubg  18917  galcan  18919  gacan  18920  cntzsubg  18952  cntzmhm  18954  symgvalstruct  19013  symgvalstructOLD  19014  psgnunilem2  19112  psgnuni  19116  sylow1lem1  19212  sylow2blem2  19235  sylow2blem3  19236  lsmmod  19290  lsmpropd  19292  lsmdisj2  19297  subgdisj1  19306  subgdisj2  19307  efgredleme  19358  efgredlemd  19359  efgredlemc  19360  efgredlem  19362  frgpup3lem  19392  mulgdi  19437  ghmcmn  19442  lsm4  19470  cygablOLD  19501  gsummhm2  19549  gsumpt  19572  gsum2d  19582  gsumcom3  19588  dprdfeq0  19634  ablfac1eu  19685  ablsimpgprmd  19727  ringcom  19827  isringd  19833  ringlz  19835  ringrz  19836  ring1eq0  19838  ringmneg1  19844  gsumdixp  19857  unitgrp  19918  irredrmul  19958  drngmul0or  20021  subrginv  20049  subrgunit  20051  primefld  20082  abvrec  20105  srngnvl  20125  srngadd  20126  srngmul  20127  issrngd  20130  lmodvs0  20166  lmodvneg1  20175  lmodcom  20178  lmodsubdi  20189  lmodvsinv  20307  lmodvsinv2  20308  lmhmvsca  20316  lvecvs0or  20379  lvecinv  20384  lspsnvs  20385  lspabs2  20391  lspfixed  20399  lspsolv  20414  unitrrg  20573  prmirredlem  20703  mulgrhm2  20709  chrrhm  20744  znidomb  20778  psgnghm  20794  psgninv  20796  zrhpsgnodpm  20806  evpmodpmf1o  20810  psgndiflemB  20814  ip0r  20851  ipdir  20853  ipdi  20854  ipass  20859  ipassr  20860  phlpropd  20869  ocvpj  20933  uvcresum  21009  lmimlbs  21052  asclpropd  21110  psrass1lemOLD  21152  psrass1lem  21155  psrlidm  21181  psrridm  21182  mvrf1  21203  mplmon2mul  21286  evlslem1  21301  evlseu  21302  evlssca  21308  evlsvar  21309  coe1pwmul  21459  pf1ind  21530  mat0dimbas0  21624  mdetrlin  21760  mdetrsca  21761  mdetr0  21763  mdetunilem8  21777  mdetuni0  21779  mdetmul  21781  maducoeval2  21798  madurid  21802  madulid  21803  matinv  21835  matunit  21836  slesolinv  21838  slesolinvbi  21839  cpmadugsumlemF  22034  restin  22326  cncmp  22552  cmpsublem  22559  conndisj  22576  cnconn  22582  kgencmp2  22706  ufldom  23122  tgplacthmeo  23263  ghmcnp  23275  qustgpopn  23280  qustgphaus  23283  tsmsxplem2  23314  tususp  23433  xpsdsval  23543  blpnfctr  23598  xmssym  23627  ressxms  23690  isngp2  23762  ngppropd  23802  nminvr  23842  blcvx  23970  icccvx  24122  pcohtpylem  24191  pcohtpy  24192  clmvscom  24262  cvsmuleqdivd  24306  cvsdiveqd  24307  pjthlem1  24610  ovollb2lem  24661  ovolicc2lem1  24690  ovolicc2lem5  24694  volsup  24729  ovolioo  24741  uniiccdif  24751  uniioombllem3  24758  uniioombllem4  24759  vitalilem3  24783  itg1sub  24883  itg2const  24914  iblcnlem1  24961  itgcnlem  24963  itgaddlem2  24997  itgsub  24999  itgabs  25008  ditgsplit  25034  dvmulbr  25112  dvcmul  25117  dvcmulf  25118  dvrec  25128  dvmptres3  25129  dvmptadd  25133  dvmptmul  25134  dvmptres2  25135  dvmptneg  25139  dvmptsub  25140  dvmptcj  25141  dvmptco  25145  dveflem  25152  dvlip  25166  dvlipcn  25167  dvlip2  25168  dvcvx  25193  dvfsumle  25194  dvfsumabs  25196  dvfsumlem1  25199  dvfsumlem2  25200  ftc2  25217  ftc2ditglem  25218  itgparts  25220  itgsubstlem  25221  itgsubst  25222  itgpowd  25223  fta1glem1  25339  fta1blem  25342  plyeq0lem  25380  plymullem1  25384  coeeulem  25394  coe0  25426  coesub  25427  dvply1  25453  plydivlem4  25465  plyrem  25474  fta1lem  25476  vieta1  25481  plyexmo  25482  elqaalem2  25489  aareccl  25495  aannenlem1  25497  aaliou3lem2  25512  dvtaylp  25538  taylthlem1  25541  radcnvlem1  25581  pserdvlem2  25596  efcvx  25617  ptolemy  25662  tangtx  25671  efif1olem3  25709  efif1olem4  25710  efabl  25715  lognegb  25754  efiarg  25771  cosargd  25772  tanarg  25783  logtayl  25824  cxpneg  25845  cxpsub  25846  cxprec  25850  cxproot  25854  cxpsqrt  25867  cxpcom  25901  cxpcn3lem  25909  cxpaddlelem  25913  abscxpbnd  25915  root1eq1  25917  cxpeq  25919  logrec  25922  isosctrlem2  25978  isosctrlem3  25979  isosctr  25980  ssscongptld  25981  chordthmlem  25991  heron  25997  quad2  25998  dcubic1lem  26002  mcubic  26006  cubic2  26007  cubic  26008  dquartlem2  26011  dquart  26012  quart1lem  26014  quart1  26015  asinlem2  26028  asinlem3  26030  asinsin  26051  sinacos  26064  atanlogsublem  26074  efiatan2  26076  2efiatan  26077  tanatan  26078  atantan  26082  atans2  26090  dvatan  26094  atantayl  26096  atantayl2  26097  log2cnv  26103  rlimcnp2  26125  cxplim  26130  cxp2lim  26135  cvxcl  26143  scvxcvx  26144  zetacvg  26173  lgamgulmlem4  26190  lgamcvg2  26213  gamp1  26216  wilthlem1  26226  wilthlem2  26227  ftalem5  26235  basellem3  26241  basellem5  26243  basellem8  26246  mumullem2  26338  musum  26349  musumsum  26350  muinv  26351  sgmppw  26354  1sgmprm  26356  1sgm2ppw  26357  ppiub  26361  logfac2  26374  chpchtsum  26376  perfectlem1  26386  perfectlem2  26387  dchrn0  26407  dchrfi  26412  dchrabs  26417  dchrptlem1  26421  dchrhash  26428  dchr2sum  26430  sum2dchr  26431  bposlem6  26446  bposlem9  26449  lgsvalmod  26473  lgsdilem  26481  lgsne0  26492  lgssq  26494  lgssq2  26495  lgsqr  26508  lgsdchrval  26511  lgsdchr  26512  gausslemma2dlem6  26529  gausslemma2d  26531  lgseisenlem1  26532  lgseisenlem2  26533  lgseisenlem4  26535  lgsquadlem1  26537  lgsquadlem3  26539  lgsquad3  26544  m1lgs  26545  2sqmod  26593  rplogsumlem1  26641  rplogsumlem2  26642  dchrisumlem2  26647  dchrisum0fno1  26668  rpvmasum2  26669  dchrisum0lem1  26673  dchrisum0lem2  26675  mudivsum  26687  mulog2sumlem1  26691  vmalogdivsum  26696  2vmadivsumlem  26697  logsqvma  26699  selberglem1  26702  selberglem2  26703  selberg2lem  26707  selberg3lem1  26714  selberg4lem1  26717  selberg4  26718  pntrsumo1  26722  selbergr  26725  selberg34r  26728  pntrlog2bndlem3  26736  pntrlog2bndlem4  26737  pntibndlem2  26748  pntlemg  26755  pntlemr  26759  pntlemf  26762  ostthlem1  26784  padicabvcxp  26789  ostth3  26795  tgcgrcomlr  26850  tgifscgr  26878  iscgrglt  26884  tgbtwnconn1lem2  26943  tgbtwnconn1lem3  26944  mirne  27037  miduniq2  27057  krippenlem  27060  ragcgr  27077  cgrg3col4  27223  f1otrg  27241  ttgcontlem1  27261  brbtwn2  27282  axsegconlem10  27303  ax5seglem3  27308  ax5seglem6  27311  axpaschlem  27317  axeuclidlem  27339  axcontlem2  27342  axcontlem7  27347  axcontlem8  27348  cusgrsizeindslem  27827  frgrncvvdeq  28682  numclwwlk7  28764  grpoidinvlem1  28875  grpoideu  28880  grporcan  28889  grpolcan  28901  grpoinvop  28904  ablo4  28921  nvscom  29000  nvmul0or  29021  nvz0  29039  smcnlem  29068  ipidsq  29081  sspz  29106  lno0  29127  lnoadd  29129  lnomul  29131  ipasslem3  29204  dipdi  29214  dipassr  29217  dipsubdi  29220  ubthlem2  29242  hvmul0or  29396  hvadd12  29406  hvadd4  29407  hvmulcom  29414  normneg  29515  pjhthlem1  29762  chj12  29905  spanunsni  29950  5oalem2  30026  3oalem2  30034  hoadd4  30155  homul12  30176  hosubdi  30179  honegsubdi  30181  hosub4  30184  adj2  30305  lnopmul  30338  lnopaddi  30342  lnfnaddi  30414  lnfnmuli  30415  cnlnadjlem6  30443  adjeq0  30462  leopmul  30505  opsqrlem1  30511  opsqrlem6  30516  hstnmoc  30594  strlem1  30621  chirredlem3  30763  reldisjun  30951  2ndresdju  30995  suppovss  31026  cosnop  31037  fpwrelmapffslem  31076  xaddeq0  31085  bcm1n  31125  divnumden2  31141  xmulcand  31204  xreceu  31205  s3f1  31230  ccatf1  31232  wrdt2ind  31234  swrdf1  31237  xrsmulgzz  31296  xrge0adddir  31310  xrge0adddi  31311  abliso  31314  gsumhashmul  31325  ogrpaddltrbid  31355  ogrpinvlt  31358  symgcom  31361  cyc2fv1  31397  cyc2fv2  31398  cycpmco2rn  31401  cycpmco2lem5  31406  cycpmco2lem6  31407  cycpmco2lem7  31408  cyc3fv1  31413  cyc3fv2  31414  cyc3fv3  31415  cycpmconjvlem  31417  cycpmconjslem2  31431  cycpmconjs  31432  cyc3conja  31433  archiabllem1a  31454  archiabllem1  31456  archiabllem2c  31458  slmdvs0  31487  dvrcan5  31499  ornglmullt  31515  orngrmullt  31516  rhmunitinv  31530  qusscaval  31561  imaslmod  31562  qustriv  31569  znfermltl  31571  quslsm  31602  nsgmgclem  31605  qsidomlem2  31638  mxidlprm  31649  ply1fermltl  31679  sradrng  31682  drgext0gsca  31688  rgmoddim  31702  matdim  31707  lbsdiflsp0  31716  dimkerim  31717  fedgmullem1  31719  fedgmullem2  31720  fedgmul  31721  extdg1id  31747  ccfldextdgrr  31751  mdetpmtr2  31783  madjusmdetlem1  31786  mdetlap  31791  qtophaus  31795  zarcmplem  31840  qqhval2lem  31940  esumpad  32032  esummulc1  32058  esumsup  32066  measxun2  32187  measssd  32192  inelcarsg  32287  carsggect  32294  carsgclctunlem2  32295  pmeasmono  32300  oddpwdc  32330  eulerpartlemgs2  32356  eulerpartlemn  32357  totprobd  32402  signstfvn  32557  signstfveq0  32565  ftc2re  32587  itgexpif  32595  breprexpnat  32623  circlemethnat  32630  circlevma  32631  circlemethhgt  32632  hgt750lemf  32642  hgt750lemg  32643  hgt750lemb  32645  tgoldbachgt  32652  bnj1379  32819  bnj1321  33016  revpfxsfxrev  33086  revwlk  33095  subfaclim  33159  cvxsconn  33214  resconn  33217  cvmliftmolem1  33252  cvmliftlem7  33262  cvmliftlem13  33267  cvmlift2lem7  33280  cvmlift3lem5  33294  elmsta  33519  msubff1  33527  mthmpps  33553  bcm1nt  33712  faclim2  33723  funsseq  33751  nolesgn2o  33883  nolesgn2ores  33884  nogesgn1o  33885  nogesgn1ores  33886  nodenselem5  33900  nolt02o  33907  nogt01o  33908  nosupprefixmo  33912  noinfprefixmo  33913  sltlpss  34096  clsun  34526  topjoin  34563  bj-bary1lem  35490  irrdifflemf  35505  finxpreclem4  35574  matunitlindflem1  35782  ptrest  35785  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem9  35795  poimirlem11  35797  poimirlem12  35798  poimirlem26  35812  poimirlem27  35813  itg2addnclem  35837  itg2addnclem3  35839  itgaddnclem2  35845  itgsubnc  35848  iblmulc2nc  35851  itgabsnc  35855  ftc2nc  35868  areacirclem1  35874  areacirclem4  35877  areacirc  35879  cocanfo  35885  ablo4pnp  36047  rngolz  36089  rngorz  36090  zerdivemp1x  36114  crngm4  36170  crngohomfo  36173  lfl0  37086  lfladd  37087  lflmul  37089  eqlkr3  37122  olm11  37248  latm12  37251  cmtcomlemN  37269  omlspjN  37282  hlatj12  37392  1cvrjat  37496  dalemrotyz  37679  padd12N  37860  pmapjlln1  37876  atmod2i1  37882  pmapocjN  37951  pnonsingN  37954  pexmidN  37990  lhp2at0  38053  lhpelim  38058  ltrncnv  38167  cdleme7c  38266  cdleme15b  38296  cdlemednpq  38320  cdleme20m  38344  cdleme22cN  38363  cdleme22d  38364  cdleme23b  38371  cdleme30a  38399  cdleme35h  38477  cdlemeg46frv  38546  cdlemg2fv2  38621  cdlemg2l  38624  cdlemg2m  38625  cdlemg8c  38650  cdlemg10bALTN  38657  cdlemg12  38671  cdlemg13a  38672  cdlemg18c  38701  cdlemg19  38705  trlcoat  38744  cdlemg47  38757  tendo1ne0  38849  cdlemk9  38860  cdlemk9bN  38861  dia2dimlem1  39085  tendolinv  39126  tendorinv  39127  dvhlveclem  39129  doca3N  39148  dihmeetlem7N  39331  dihjatc1  39332  dihmeetlem18N  39345  dochnoncon  39412  dihjatc  39438  dihjatcclem1  39439  dihjatcclem4  39442  dochsnkr  39493  lcfl7lem  39520  lcfl8  39523  lcfl9a  39526  lclkrlem1  39527  lclkrlem2e  39532  lclkrlem2j  39537  lcfrlem1  39563  lcfrlem9  39571  lcfrlem23  39586  lcfrlem31  39594  mapd0  39686  mapdpglem21  39713  baerlem3lem1  39728  baerlem5alem1  39729  mapdindp4  39744  mapdh6gN  39763  hdmap1l6g  39837  hgmapval0  39913  hgmaprnlem1N  39917  hlhilhillem  39985  drngmulcanad  40259  drngmulcan2ad  40260  drnginvmuld  40261  pwsexpg  40275  mhphf  40292  sn-1ne2  40302  exp11d  40332  numdenexp  40344  resubeulem2  40366  resubidaddid1lem  40384  sn-00idlem1  40388  readdcan2  40402  sn-negex12  40405  sn-addcand  40408  remulinvcom  40421  remulid2  40422  remulcand  40427  sn-0tie0  40428  retire  40444  cnreeu  40445  prjspner1  40470  dffltz  40478  flt4lem5f  40501  flt4lem7  40503  fltnltalem  40506  fltnlta  40507  diophrw  40588  eldioph2lem1  40589  pellexlem2  40659  pellexlem6  40663  pellex  40664  pell1234qrne0  40682  pell1234qrreccl  40683  pell1qrgaplem  40702  rmxm1  40763  oddcomabszz  40773  jm2.19lem1  40818  jm3.1lem2  40847  dnnumch3  40879  pwssplit4  40921  flcidc  41006  deg1mhm  41039  sqrtcval  41256  radcnvrat  41939  nzprmdif  41944  hashnzfz  41945  dvsconst  41955  dvsid  41956  expgrowth  41960  bccm1k  41967  bccn1  41969  binomcxplemnotnn0  41981  subadd4b  42828  uzinico2  43107  sumnnodd  43178  limsupresuz  43251  limsupequzlem  43270  liminfresre  43327  liminfresuz  43332  climliminflimsupd  43349  icccncfext  43435  dvresntr  43466  itgsinexplem1  43502  itgsinexp  43503  stoweidlem1  43549  wallispi2lem2  43620  stirlinglem3  43624  stirlinglem5  43626  stirlinglem10  43631  stirlinglem15  43636  dirkertrigeqlem3  43648  dirkercncflem2  43652  fourierdlem26  43681  fourierdlem42  43697  fourierdlem66  43720  fourierdlem73  43727  fourierdlem81  43735  fourierdlem83  43737  fourierdlem107  43761  etransclem23  43805  meaiininclem  44031  vonvolmbl  44206  iccvonmbllem  44223  sigaradd  44393  cevathlem1  44394  imarnf1pr  44785  m1mod0mod1  44832  fmtnorec3  45011  proththd  45077  perfectALTVlem1  45184  perfectALTVlem2  45185  rnglz  45453  pw2m1lepw2m1  45872  nnpw2pmod  45940  dignn0flhalflem1  45972  affinecomb2  46060  1subrec1sub  46062  eenglngeehlnmlem1  46094  2itscplem3  46137  restcls2  46218  aacllem  46516  amgmlemALT  46518  young2d  46520