Theorem 3eqtr3d 2664

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

Syntax hints:   → wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  mpteqb  6299  fvmptt  6300  fsnunfv  6453  f1ocnvfv1  6532  f1ocnvfv2  6533  fcof1  6542  weniso  6604  caov12d  6855  caov13d  6857  caov411d  6859  caovmo  6871  grprinvlem  6872  grprinvd  6873  grpridd  6874  onovuni  7439  tfrlem5  7476  seqomlem1  7545  seqomlem4  7548  onasuc  7608  onesuc  7610  oeeui  7682  fopwdom  8068  unxpdomlem2  8165  cantnfres  8574  cnfcom2lem  8598  cnfcom2  8599  cardiun  8808  ackbij1lem16  9057  ackbij2lem2  9062  fpwwe2lem6  9457  fpwwe2lem8  9459  canthp1lem2  9475  mul12  10202  mul4  10205  addid1  10216  addcan  10220  addcom  10222  addcomd  10238  add12  10253  ppncan  10323  addsub4  10324  subaddeqd  10446  muladd  10462  mulcand  10660  receu  10672  div13  10706  divdivdiv  10726  divcan5  10727  divdiv1  10736  divdiv2  10737  halfaddsub  11265  xadddi  12125  xov1plusxeqvd  12318  fztp  12397  flzadd  12627  fldiv  12659  mulp1mod1  12711  modnegd  12725  modsub12d  12727  2submod  12731  seqm1  12818  seqcaopr  12838  seqf1o  12842  exprec  12901  expsub  12908  zesq  12987  digit1  12998  discr1  13000  discr  13001  facnn2  13069  faclbnd6  13086  hashfz1  13134  hashdom  13168  hashun  13171  hashbclem  13236  hashfac  13242  seqcoll  13248  ccatopth  13470  repsw2  13693  repsw3  13694  shftval3  13816  crre  13854  resub  13867  imsub  13875  cjsub  13889  abslem2  14079  sqreulem  14099  climshft2  14313  isercolllem2  14396  iseraltlem2  14413  iseraltlem3  14414  fsumsub  14520  telfsumo  14534  telfsumo2  14535  hashiun  14554  bcxmas  14567  climcndslem1  14581  climcndslem2  14582  trireciplem  14594  geoser  14599  geo2sum2  14605  fprodm1  14697  fallfacfwd  14767  binomfallfaclem2  14771  bpolydiflem  14785  bpoly4  14790  fsumcube  14791  sinsub  14898  cossub  14899  rpnnen2lem10  14952  ruclem12  14970  mod2eq1n2dvds  15071  pwp1fsum  15114  divalglem9  15124  bitsinv1lem  15163  bitsinv1  15164  bitsf1  15168  sadasslem  15192  bitsres  15195  smup1  15211  smumul  15215  modgcd  15253  absmulgcd  15266  gcdmultiplez  15270  eucalg  15300  lcmgcd  15320  lcmid  15322  lcmftp  15349  numdensq  15462  dfphi2  15479  phiprm  15482  fermltl  15489  prmdiveq  15491  hashgcdlem  15493  odzdvds  15500  powm2modprm  15508  modprm0  15510  coprimeprodsq  15513  pythagtriplem6  15526  pythagtriplem7  15527  pythagtriplem12  15531  pythagtriplem16  15535  pcaddlem  15592  sumhash  15600  pcfac  15603  pockthlem  15609  prmreclem6  15625  4sqlem12  15660  4sqlem15  15663  vdwlem3  15687  vdwlem6  15690  vdwlem9  15693  ramub1lem2  15731  cshwshashlem2  15803  qusaddvallem  16211  xpsaddlem  16235  xpsvsca  16239  mrcun  16282  homfeqval  16357  comfeqval  16368  sectcan  16415  sectco  16416  sectmon  16442  monsect  16443  funcsect  16532  setcmon  16737  resscatc  16755  catciso  16757  evlfcllem  16861  curf2cl  16871  curfcl  16872  yonedalem4c  16917  yonedalem3b  16919  yonedainv  16921  latj12  17096  mnd12g  17306  resmhm  17359  pwsco2mhm  17371  frmdup3lem  17403  grprcan  17455  grplcan  17477  grpasscan1  17478  grpinv11  17484  grpinvnz  17486  grplmulf1o  17489  grpinvpropd  17490  grpinvadd  17493  grpsubsub4  17508  dfgrp3  17514  imasgrp2  17530  mhmid  17536  mhmmnd  17537  mulgz  17568  mulgdirlem  17572  mulgdir  17573  mulgass  17579  mulgsubdir  17582  mulgpropd  17584  pwsmulg  17587  isnsg3  17628  nmzsubg  17635  ssnmz  17636  eqger  17644  eqglact  17645  ghminv  17667  conjnmz  17694  subgga  17733  gasubg  17735  galcan  17737  gacan  17738  cntzsubg  17769  cntzmhm  17771  psgnunilem2  17915  sylow1lem1  18013  sylow2blem2  18036  sylow2blem3  18037  lsmmod  18088  lsmpropd  18090  lsmdisj2  18095  subgdisj1  18104  subgdisj2  18105  efgredleme  18156  efgredlemd  18157  efgredlemc  18158  efgredlem  18160  frgpup3lem  18190  mulgdi  18232  ghmcmn  18237  lsm4  18263  cygabl  18292  gsummhm2  18339  gsumpt  18361  gsum2d  18371  dprdfeq0  18421  ablfac1eu  18472  ringcom  18579  isringd  18585  ringlz  18587  ringrz  18588  ring1eq0  18590  ringmneg1  18596  gsumdixp  18609  unitgrp  18667  irredrmul  18707  drngmul0or  18768  subrginv  18796  subrgunit  18798  abvrec  18836  srngnvl  18856  srngadd  18857  srngmul  18858  issrngd  18861  lmodvs0  18897  lmodvneg1  18906  lmodcom  18909  lmodsubdi  18920  lmodvsinv  19036  lmodvsinv2  19037  lmhmvsca  19045  lvecvs0or  19108  lvecinv  19113  lspsnvs  19114  lspabs2  19120  lspfixed  19128  lspsolv  19143  unitrrg  19293  asclpropd  19346  psrass1lem  19377  psrlidm  19403  psrridm  19404  mvrf1  19425  mplmon2mul  19501  evlslem1  19515  evlseu  19516  evlssca  19522  evlsvar  19523  coe1pwmul  19649  pf1ind  19719  prmirredlem  19841  mulgrhm2  19847  chrrhm  19879  znidomb  19910  psgnghm  19926  psgninv  19928  zrhpsgnodpm  19938  evpmodpmf1o  19942  psgndiflemB  19946  ip0r  19982  ipdir  19984  ipdi  19985  ipass  19990  ipassr  19991  phlpropd  20000  ocvpj  20061  uvcresum  20132  lmimlbs  20175  gsumcom3  20205  mat0dimbas0  20272  mdetrlin  20408  mdetrsca  20409  mdetr0  20411  mdetunilem8  20425  mdetuni0  20427  mdetmul  20429  maducoeval2  20446  madurid  20450  madulid  20451  matinv  20483  matunit  20484  slesolinv  20486  slesolinvbi  20487  cpmadugsumlemF  20681  restin  20970  cncmp  21195  cmpsublem  21202  conndisj  21219  cnconn  21225  kgencmp2  21349  ufldom  21766  tgplacthmeo  21907  ghmcnp  21918  qustgpopn  21923  qustgphaus  21926  tsmsxplem2  21957  tususp  22076  xpsdsval  22186  blpnfctr  22241  xmssym  22270  ressxms  22330  isngp2  22401  ngppropd  22441  nminvr  22473  blcvx  22601  icccvx  22749  pcohtpylem  22819  pcohtpy  22820  clmvscom  22890  cvsmuleqdivd  22934  cvsdiveqd  22935  pjthlem1  23208  ovollb2lem  23256  ovolicc2lem1  23285  ovolicc2lem5  23289  volsup  23324  ovolioo  23336  uniiccdif  23346  uniioombllem3  23353  uniioombllem4  23354  vitalilem3  23379  itg1sub  23476  itg2const  23507  iblcnlem1  23554  itgcnlem  23556  itgaddlem2  23590  itgsub  23592  itgabs  23601  ditgsplit  23625  dvmulbr  23702  dvcmul  23707  dvcmulf  23708  dvrec  23718  dvmptres3  23719  dvmptadd  23723  dvmptmul  23724  dvmptres2  23725  dvmptneg  23729  dvmptsub  23730  dvmptcj  23731  dvmptco  23735  dveflem  23742  dvlip  23756  dvlipcn  23757  dvlip2  23758  dvcvx  23783  dvfsumle  23784  dvfsumabs  23786  dvfsumlem1  23789  dvfsumlem2  23790  ftc2  23807  ftc2ditglem  23808  itgparts  23810  itgsubstlem  23811  itgsubst  23812  fta1glem1  23925  fta1blem  23928  plyeq0lem  23966  plymullem1  23970  coeeulem  23980  coe0  24012  coesub  24013  dvply1  24039  plydivlem4  24051  plyrem  24060  fta1lem  24062  vieta1  24067  plyexmo  24068  elqaalem2  24075  aareccl  24081  aannenlem1  24083  aaliou3lem2  24098  dvtaylp  24124  taylthlem1  24127  radcnvlem1  24167  pserdvlem2  24182  efcvx  24203  ptolemy  24248  tangtx  24257  efif1olem3  24290  efif1olem4  24291  efabl  24296  lognegb  24336  efiarg  24353  cosargd  24354  tanarg  24365  logtayl  24406  cxpneg  24427  cxpsub  24428  cxprec  24432  cxproot  24436  cxpsqrt  24449  cxpcn3lem  24488  cxpaddlelem  24492  abscxpbnd  24494  root1eq1  24496  cxpeq  24498  logrec  24501  isosctrlem2  24549  isosctrlem3  24550  isosctr  24551  ssscongptld  24552  chordthmlem  24559  heron  24565  quad2  24566  dcubic1lem  24570  mcubic  24574  cubic2  24575  cubic  24576  dquartlem2  24579  dquart  24580  quart1lem  24582  quart1  24583  asinlem2  24596  asinlem3  24598  asinsin  24619  sinacos  24632  atanlogsublem  24642  efiatan2  24644  2efiatan  24645  tanatan  24646  atantan  24650  atans2  24658  dvatan  24662  atantayl  24664  atantayl2  24665  log2cnv  24671  rlimcnp2  24693  cxplim  24698  cxp2lim  24703  cvxcl  24711  scvxcvx  24712  zetacvg  24741  lgamgulmlem4  24758  lgamcvg2  24781  gamp1  24784  wilthlem1  24794  wilthlem2  24795  ftalem5  24803  basellem3  24809  basellem5  24811  basellem8  24814  mumullem2  24906  musum  24917  musumsum  24918  muinv  24919  sgmppw  24922  1sgmprm  24924  1sgm2ppw  24925  ppiub  24929  logfac2  24942  chpchtsum  24944  perfectlem1  24954  perfectlem2  24955  dchrn0  24975  dchrfi  24980  dchrabs  24985  dchrptlem1  24989  dchrhash  24996  dchr2sum  24998  sum2dchr  24999  bposlem6  25014  bposlem9  25017  lgsvalmod  25041  lgsdilem  25049  lgsne0  25060  lgssq  25062  lgssq2  25063  lgsqr  25076  lgsdchrval  25079  lgsdchr  25080  gausslemma2dlem6  25097  gausslemma2d  25099  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem4  25103  lgsquadlem1  25105  lgsquadlem3  25107  lgsquad3  25112  m1lgs  25113  rplogsumlem1  25173  rplogsumlem2  25174  dchrisumlem2  25179  dchrisum0fno1  25200  rpvmasum2  25201  dchrisum0lem1  25205  dchrisum0lem2  25207  mudivsum  25219  mulog2sumlem1  25223  vmalogdivsum  25228  2vmadivsumlem  25229  logsqvma  25231  selberglem2  25235  selberg2lem  25239  selberg3lem1  25246  selberg4lem1  25249  selberg4  25250  pntrsumo1  25254  selbergr  25257  selberg34r  25260  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntibndlem2  25280  pntlemg  25287  pntlemr  25291  pntlemf  25294  ostthlem1  25316  padicabvcxp  25321  ostth3  25327  tgcgrcomlr  25375  tgifscgr  25403  iscgrglt  25409  tgbtwnconn1lem2  25468  tgbtwnconn1lem3  25469  mirne  25562  miduniq2  25582  krippenlem  25585  ragcgr  25602  cgrg3col4  25734  f1otrg  25751  ttgcontlem1  25765  brbtwn2  25785  axsegconlem10  25806  ax5seglem3  25811  ax5seglem6  25814  axpaschlem  25820  axeuclidlem  25842  axcontlem2  25845  axcontlem7  25850  axcontlem8  25851  cusgrsizeindslem  26347  frgrncvvdeq  27173  numclwwlk7  27249  grpoidinvlem1  27358  grpoideu  27363  grporcan  27372  grpolcan  27384  grpoinvop  27387  ablo4  27404  nvscom  27484  nvmul0or  27505  nvz0  27523  smcnlem  27552  ipidsq  27565  sspz  27590  lno0  27611  lnoadd  27613  lnomul  27615  ipasslem3  27688  dipdi  27698  dipassr  27701  dipsubdi  27704  ubthlem2  27727  hvmul0or  27882  hvadd12  27892  hvadd4  27893  hvmulcom  27900  normneg  28001  pjhthlem1  28250  chj12  28393  spanunsni  28438  5oalem2  28514  3oalem2  28522  hoadd4  28643  homul12  28664  hosubdi  28667  honegsubdi  28669  hosub4  28672  adj2  28793  lnopmul  28826  lnopaddi  28830  lnfnaddi  28902  lnfnmuli  28903  cnlnadjlem6  28931  adjeq0  28950  leopmul  28993  opsqrlem1  28999  opsqrlem6  29004  hstnmoc  29082  strlem1  29109  chirredlem3  29251  fpwrelmapffslem  29507  subeqxfrd  29511  xaddeq0  29518  bcm1n  29554  divnumden2  29564  xmulcand  29629  xreceu  29630  bhmafibid1  29644  2sqmod  29648  xrsmulgzz  29678  xrge0adddir  29692  xrge0adddi  29693  abliso  29696  ogrpaddltrbid  29721  ogrpinvlt  29724  archiabllem1a  29745  archiabllem1  29747  archiabllem2c  29749  slmdvs0  29778  dvrcan5  29793  ornglmullt  29807  orngrmullt  29808  rhmunitinv  29822  mdetpmtr2  29890  madjusmdetlem1  29893  mdetlap  29898  qtophaus  29903  qqhval2lem  30025  esumpad  30117  esummulc1  30143  esumsup  30151  measxun2  30273  measssd  30278  inelcarsg  30373  carsggect  30380  carsgclctunlem2  30381  pmeasmono  30386  oddpwdc  30416  eulerpartlemgs2  30442  eulerpartlemn  30443  totprobd  30488  signstfvn  30646  signstfveq0  30654  ftc2re  30676  itgexpif  30684  breprexpnat  30712  circlemethnat  30719  circlevma  30720  circlemethhgt  30721  hgt750lemf  30731  hgt750lemg  30732  hgt750lemb  30734  tgoldbachgt  30741  bnj1379  30901  bnj1321  31095  subfaclim  31170  cvxsconn  31225  resconn  31228  cvmliftmolem1  31263  cvmliftlem7  31273  cvmliftlem13  31278  cvmlift2lem7  31291  cvmlift3lem5  31305  elmsta  31445  msubff1  31453  mthmpps  31479  bcm1nt  31623  faclim2  31634  funsseq  31666  nolesgn2o  31824  nolesgn2ores  31825  nodenselem5  31838  nolt02o  31845  noprefixmo  31848  clsun  32323  topjoin  32360  bj-bary1lem  33160  finxpreclem4  33231  matunitlindflem1  33405  ptrest  33408  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem9  33418  poimirlem11  33420  poimirlem12  33421  poimirlem26  33435  poimirlem27  33436  itg2addnclem  33461  itg2addnclem3  33463  itgaddnclem2  33469  itgsubnc  33472  iblmulc2nc  33475  itgabsnc  33479  ftc2nc  33494  areacirclem1  33500  areacirclem4  33503  areacirc  33505  cocanfo  33512  ablo4pnp  33679  rngolz  33721  rngorz  33722  zerdivemp1x  33746  crngm4  33802  crngohomfo  33805  fsumshftdOLD  34238  lfl0  34352  lfladd  34353  lflmul  34355  eqlkr3  34388  olm11  34514  latm12  34517  cmtcomlemN  34535  omlspjN  34548  hlatj12  34657  1cvrjat  34761  dalemrotyz  34944  padd12N  35125  pmapjlln1  35141  atmod2i1  35147  pmapocjN  35216  pnonsingN  35219  pexmidN  35255  lhp2at0  35318  lhpelim  35323  ltrncnv  35432  ltrnmwOLD  35438  cdleme7c  35532  cdleme15b  35562  cdlemednpq  35586  cdleme20yOLD  35590  cdleme20m  35611  cdleme22cN  35630  cdleme22d  35631  cdleme23b  35638  cdleme30a  35666  cdleme35h  35744  cdlemeg46frv  35813  cdlemg2fv2  35888  cdlemg2l  35891  cdlemg2m  35892  cdlemg8c  35917  cdlemg10bALTN  35924  cdlemg12  35938  cdlemg13a  35939  cdlemg18c  35968  cdlemg19  35972  trlcoat  36011  cdlemg47  36024  tendo1ne0  36116  cdlemk9  36127  cdlemk9bN  36128  dia2dimlem1  36353  tendolinv  36394  tendorinv  36395  dvhlveclem  36397  doca3N  36416  dihmeetlem7N  36599  dihjatc1  36600  dihmeetlem18N  36613  dochnoncon  36680  dihjatc  36706  dihjatcclem1  36707  dihjatcclem4  36710  dochsnkr  36761  lcfl7lem  36788  lcfl8  36791  lcfl9a  36794  lclkrlem1  36795  lclkrlem2e  36800  lclkrlem2j  36805  lcfrlem1  36831  lcfrlem9  36839  lcfrlem23  36854  lcfrlem31  36862  mapd0  36954  mapdpglem21  36981  baerlem3lem1  36996  baerlem5alem1  36997  mapdindp4  37012  mapdh6gN  37031  hdmap1l6g  37106  hgmapval0  37184  hgmaprnlem1N  37188  hlhilhillem  37252  diophrw  37322  eldioph2lem1  37323  pellexlem2  37394  pellexlem6  37398  pellex  37399  pell1234qrne0  37417  pell1234qrreccl  37418  pell1qrgaplem  37437  rmxm1  37499  oddcomabszz  37509  jm2.19lem1  37556  jm3.1lem2  37585  dnnumch3  37617  pwssplit4  37659  flcidc  37744  deg1mhm  37785  itgpowd  37800  radcnvrat  38513  nzprmdif  38518  hashnzfz  38519  dvsconst  38529  dvsid  38530  expgrowth  38534  bccm1k  38541  bccn1  38543  binomcxplemnotnn0  38555  subadd4b  39494  uzinico2  39789  sumnnodd  39862  limsupresuz  39935  limsupequzlem  39954  liminfresre  40011  liminfresuz  40016  climliminflimsupd  40033  icccncfext  40100  dvresntr  40132  itgsinexplem1  40169  itgsinexp  40170  stoweidlem1  40218  wallispi2lem2  40289  stirlinglem3  40293  stirlinglem5  40295  stirlinglem10  40300  stirlinglem15  40305  dirkertrigeqlem3  40317  dirkercncflem2  40321  fourierdlem26  40350  fourierdlem42  40366  fourierdlem66  40389  fourierdlem73  40396  fourierdlem81  40404  fourierdlem83  40406  fourierdlem107  40430  etransclem23  40474  meaiininclem  40700  vonvolmbl  40875  iccvonmbllem  40892  sigaradd  41055  cevathlem1  41056  imarnf1pr  41301  m1mod0mod1  41339  fmtnorec3  41460  proththd  41531  perfectALTVlem1  41630  perfectALTVlem2  41631  rnglz  41884  pw2m1lepw2m1  42310  nnpw2pmod  42377  dignn0flhalflem1  42409  aacllem  42547  amgmlemALT  42549  young2d  42551