Theorem 3eqtr3d 2786

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 2780	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
4		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	eqtr3d 2780	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 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  mpteqb  6876  fvmptt  6877  fvsnun2  7037  fsnunfv  7041  f1ocnvfv1  7129  f1ocnvfv2  7130  fcof1  7139  f1ofvswap  7158  weniso  7205  caov12d  7471  caov13d  7473  caov411d  7475  caovmo  7487  onovuni  8144  tfrlem5  8182  seqomlem1  8251  seqomlem4  8254  onasuc  8320  onesuc  8322  oeeui  8395  fopwdom  8820  unxpdomlem2  8957  cantnfres  9365  cnfcom2lem  9389  cnfcom2  9390  updjud  9623  cardiun  9671  ackbij1lem16  9922  ackbij2lem2  9927  fpwwe2lem5  10322  fpwwe2lem7  10324  canthp1lem2  10340  mul12  11070  mul4  11073  addid1  11085  addcan  11089  addcom  11091  addcomd  11107  add12  11122  ppncan  11193  addsub4  11194  subeqxfrd  11314  subaddeqd  11320  muladd  11337  mulcand  11538  receu  11550  div13  11584  divdivdiv  11606  divcan5  11607  divdiv1  11616  divdiv2  11617  halfaddsub  12136  xadddi  12958  xov1plusxeqvd  13159  fztp  13241  flzadd  13474  fldiv  13508  mulp1mod1  13560  modnegd  13574  modsub12d  13576  2submod  13580  seqm1  13668  seqcaopr  13688  seqf1o  13692  exprec  13752  expsub  13759  zesq  13869  digit1  13880  discr1  13882  discr  13883  facnn2  13924  faclbnd6  13941  hashfz1  13988  hashdom  14022  hashun  14025  hashbclem  14092  hashfac  14100  seqcoll  14106  ccatopth  14357  repsw2  14591  repsw3  14592  shftval3  14715  crre  14753  resub  14766  imsub  14774  cjsub  14788  nn0sqeq1  14916  abslem2  14979  sqreulem  14999  bhmafibid1  15105  climshft2  15219  isercolllem2  15305  iseraltlem2  15322  iseraltlem3  15323  fsumsub  15428  telfsumo  15442  telfsumo2  15443  hashiun  15462  bcxmas  15475  climcndslem1  15489  climcndslem2  15490  trireciplem  15502  geoser  15507  geo2sum2  15514  fprodm1  15605  fallfacfwd  15674  binomfallfaclem2  15678  bpolydiflem  15692  bpoly4  15697  fsumcube  15698  sinsub  15805  cossub  15806  rpnnen2lem10  15860  ruclem12  15878  p1modz1  15898  mod2eq1n2dvds  15984  pwp1fsum  16028  divalglem9  16038  bitsinv1lem  16076  bitsinv1  16077  bitsf1  16081  sadasslem  16105  bitsres  16108  smup1  16124  smumul  16128  modgcd  16168  absmulgcd  16185  gcdmultiplezOLD  16189  eucalg  16220  lcmgcd  16240  lcmid  16242  lcmftp  16269  numdensq  16386  dfphi2  16403  phiprm  16406  fermltl  16413  prmdiveq  16415  hashgcdlem  16417  odzdvds  16424  powm2modprm  16432  modprm0  16434  coprimeprodsq  16437  pythagtriplem6  16450  pythagtriplem7  16451  pythagtriplem12  16455  pythagtriplem16  16459  pcaddlem  16517  sumhash  16525  pcfac  16528  pockthlem  16534  prmreclem6  16550  4sqlem12  16585  4sqlem15  16588  vdwlem3  16612  vdwlem6  16615  vdwlem9  16618  ramub1lem2  16656  cshwshashlem2  16726  qusaddvallem  17179  xpsaddlem  17201  xpsvsca  17205  mrcun  17248  homfeqval  17323  comfeqval  17334  sectcan  17384  sectco  17385  sectmon  17411  monsect  17412  funcsect  17503  setcmon  17718  resscatc  17740  catciso  17742  evlfcllem  17855  curf2cl  17865  curfcl  17866  yonedalem4c  17911  yonedalem3b  17913  yonedainv  17915  latj12  18117  grprinvlem  18272  grprinvd  18273  grpridd  18274  mnd12g  18313  resmhm  18374  pwsco2mhm  18386  frmdup3lem  18420  grprcan  18528  grplcan  18552  grpasscan1  18553  grpinv11  18559  grpinvnz  18561  grplmulf1o  18564  grpinvpropd  18565  grpinvadd  18568  grpsubsub4  18583  dfgrp3  18589  imasgrp2  18605  mhmid  18611  mhmmnd  18612  mulgz  18646  mulgdirlem  18649  mulgdir  18650  mulgass  18655  mulgsubdir  18658  mulgpropd  18660  pwsmulg  18663  isnsg3  18703  nmzsubg  18708  ssnmz  18709  eqger  18721  eqglact  18722  cyccom  18737  ghminv  18756  conjnmz  18783  subgga  18821  gasubg  18823  galcan  18825  gacan  18826  cntzsubg  18858  cntzmhm  18860  symgvalstruct  18919  symgvalstructOLD  18920  psgnunilem2  19018  psgnuni  19022  sylow1lem1  19118  sylow2blem2  19141  sylow2blem3  19142  lsmmod  19196  lsmpropd  19198  lsmdisj2  19203  subgdisj1  19212  subgdisj2  19213  efgredleme  19264  efgredlemd  19265  efgredlemc  19266  efgredlem  19268  frgpup3lem  19298  mulgdi  19343  ghmcmn  19348  lsm4  19376  cygablOLD  19407  gsummhm2  19455  gsumpt  19478  gsum2d  19488  gsumcom3  19494  dprdfeq0  19540  ablfac1eu  19591  ablsimpgprmd  19633  ringcom  19733  isringd  19739  ringlz  19741  ringrz  19742  ring1eq0  19744  ringmneg1  19750  gsumdixp  19763  unitgrp  19824  irredrmul  19864  drngmul0or  19927  subrginv  19955  subrgunit  19957  primefld  19988  abvrec  20011  srngnvl  20031  srngadd  20032  srngmul  20033  issrngd  20036  lmodvs0  20072  lmodvneg1  20081  lmodcom  20084  lmodsubdi  20095  lmodvsinv  20213  lmodvsinv2  20214  lmhmvsca  20222  lvecvs0or  20285  lvecinv  20290  lspsnvs  20291  lspabs2  20297  lspfixed  20305  lspsolv  20320  unitrrg  20477  prmirredlem  20606  mulgrhm2  20612  chrrhm  20647  znidomb  20681  psgnghm  20697  psgninv  20699  zrhpsgnodpm  20709  evpmodpmf1o  20713  psgndiflemB  20717  ip0r  20754  ipdir  20756  ipdi  20757  ipass  20762  ipassr  20763  phlpropd  20772  ocvpj  20834  uvcresum  20910  lmimlbs  20953  asclpropd  21011  psrass1lemOLD  21053  psrass1lem  21056  psrlidm  21082  psrridm  21083  mvrf1  21104  mplmon2mul  21187  evlslem1  21202  evlseu  21203  evlssca  21209  evlsvar  21210  coe1pwmul  21360  pf1ind  21431  mat0dimbas0  21523  mdetrlin  21659  mdetrsca  21660  mdetr0  21662  mdetunilem8  21676  mdetuni0  21678  mdetmul  21680  maducoeval2  21697  madurid  21701  madulid  21702  matinv  21734  matunit  21735  slesolinv  21737  slesolinvbi  21738  cpmadugsumlemF  21933  restin  22225  cncmp  22451  cmpsublem  22458  conndisj  22475  cnconn  22481  kgencmp2  22605  ufldom  23021  tgplacthmeo  23162  ghmcnp  23174  qustgpopn  23179  qustgphaus  23182  tsmsxplem2  23213  tususp  23332  xpsdsval  23442  blpnfctr  23497  xmssym  23526  ressxms  23587  isngp2  23659  ngppropd  23699  nminvr  23739  blcvx  23867  icccvx  24019  pcohtpylem  24088  pcohtpy  24089  clmvscom  24159  cvsmuleqdivd  24203  cvsdiveqd  24204  pjthlem1  24506  ovollb2lem  24557  ovolicc2lem1  24586  ovolicc2lem5  24590  volsup  24625  ovolioo  24637  uniiccdif  24647  uniioombllem3  24654  uniioombllem4  24655  vitalilem3  24679  itg1sub  24779  itg2const  24810  iblcnlem1  24857  itgcnlem  24859  itgaddlem2  24893  itgsub  24895  itgabs  24904  ditgsplit  24930  dvmulbr  25008  dvcmul  25013  dvcmulf  25014  dvrec  25024  dvmptres3  25025  dvmptadd  25029  dvmptmul  25030  dvmptres2  25031  dvmptneg  25035  dvmptsub  25036  dvmptcj  25037  dvmptco  25041  dveflem  25048  dvlip  25062  dvlipcn  25063  dvlip2  25064  dvcvx  25089  dvfsumle  25090  dvfsumabs  25092  dvfsumlem1  25095  dvfsumlem2  25096  ftc2  25113  ftc2ditglem  25114  itgparts  25116  itgsubstlem  25117  itgsubst  25118  itgpowd  25119  fta1glem1  25235  fta1blem  25238  plyeq0lem  25276  plymullem1  25280  coeeulem  25290  coe0  25322  coesub  25323  dvply1  25349  plydivlem4  25361  plyrem  25370  fta1lem  25372  vieta1  25377  plyexmo  25378  elqaalem2  25385  aareccl  25391  aannenlem1  25393  aaliou3lem2  25408  dvtaylp  25434  taylthlem1  25437  radcnvlem1  25477  pserdvlem2  25492  efcvx  25513  ptolemy  25558  tangtx  25567  efif1olem3  25605  efif1olem4  25606  efabl  25611  lognegb  25650  efiarg  25667  cosargd  25668  tanarg  25679  logtayl  25720  cxpneg  25741  cxpsub  25742  cxprec  25746  cxproot  25750  cxpsqrt  25763  cxpcom  25797  cxpcn3lem  25805  cxpaddlelem  25809  abscxpbnd  25811  root1eq1  25813  cxpeq  25815  logrec  25818  isosctrlem2  25874  isosctrlem3  25875  isosctr  25876  ssscongptld  25877  chordthmlem  25887  heron  25893  quad2  25894  dcubic1lem  25898  mcubic  25902  cubic2  25903  cubic  25904  dquartlem2  25907  dquart  25908  quart1lem  25910  quart1  25911  asinlem2  25924  asinlem3  25926  asinsin  25947  sinacos  25960  atanlogsublem  25970  efiatan2  25972  2efiatan  25973  tanatan  25974  atantan  25978  atans2  25986  dvatan  25990  atantayl  25992  atantayl2  25993  log2cnv  25999  rlimcnp2  26021  cxplim  26026  cxp2lim  26031  cvxcl  26039  scvxcvx  26040  zetacvg  26069  lgamgulmlem4  26086  lgamcvg2  26109  gamp1  26112  wilthlem1  26122  wilthlem2  26123  ftalem5  26131  basellem3  26137  basellem5  26139  basellem8  26142  mumullem2  26234  musum  26245  musumsum  26246  muinv  26247  sgmppw  26250  1sgmprm  26252  1sgm2ppw  26253  ppiub  26257  logfac2  26270  chpchtsum  26272  perfectlem1  26282  perfectlem2  26283  dchrn0  26303  dchrfi  26308  dchrabs  26313  dchrptlem1  26317  dchrhash  26324  dchr2sum  26326  sum2dchr  26327  bposlem6  26342  bposlem9  26345  lgsvalmod  26369  lgsdilem  26377  lgsne0  26388  lgssq  26390  lgssq2  26391  lgsqr  26404  lgsdchrval  26407  lgsdchr  26408  gausslemma2dlem6  26425  gausslemma2d  26427  lgseisenlem1  26428  lgseisenlem2  26429  lgseisenlem4  26431  lgsquadlem1  26433  lgsquadlem3  26435  lgsquad3  26440  m1lgs  26441  2sqmod  26489  rplogsumlem1  26537  rplogsumlem2  26538  dchrisumlem2  26543  dchrisum0fno1  26564  rpvmasum2  26565  dchrisum0lem1  26569  dchrisum0lem2  26571  mudivsum  26583  mulog2sumlem1  26587  vmalogdivsum  26592  2vmadivsumlem  26593  logsqvma  26595  selberglem1  26598  selberglem2  26599  selberg2lem  26603  selberg3lem1  26610  selberg4lem1  26613  selberg4  26614  pntrsumo1  26618  selbergr  26621  selberg34r  26624  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntibndlem2  26644  pntlemg  26651  pntlemr  26655  pntlemf  26658  ostthlem1  26680  padicabvcxp  26685  ostth3  26691  tgcgrcomlr  26745  tgifscgr  26773  iscgrglt  26779  tgbtwnconn1lem2  26838  tgbtwnconn1lem3  26839  mirne  26932  miduniq2  26952  krippenlem  26955  ragcgr  26972  cgrg3col4  27118  f1otrg  27136  ttgcontlem1  27155  brbtwn2  27176  axsegconlem10  27197  ax5seglem3  27202  ax5seglem6  27205  axpaschlem  27211  axeuclidlem  27233  axcontlem2  27236  axcontlem7  27241  axcontlem8  27242  cusgrsizeindslem  27721  frgrncvvdeq  28574  numclwwlk7  28656  grpoidinvlem1  28767  grpoideu  28772  grporcan  28781  grpolcan  28793  grpoinvop  28796  ablo4  28813  nvscom  28892  nvmul0or  28913  nvz0  28931  smcnlem  28960  ipidsq  28973  sspz  28998  lno0  29019  lnoadd  29021  lnomul  29023  ipasslem3  29096  dipdi  29106  dipassr  29109  dipsubdi  29112  ubthlem2  29134  hvmul0or  29288  hvadd12  29298  hvadd4  29299  hvmulcom  29306  normneg  29407  pjhthlem1  29654  chj12  29797  spanunsni  29842  5oalem2  29918  3oalem2  29926  hoadd4  30047  homul12  30068  hosubdi  30071  honegsubdi  30073  hosub4  30076  adj2  30197  lnopmul  30230  lnopaddi  30234  lnfnaddi  30306  lnfnmuli  30307  cnlnadjlem6  30335  adjeq0  30354  leopmul  30397  opsqrlem1  30403  opsqrlem6  30408  hstnmoc  30486  strlem1  30513  chirredlem3  30655  reldisjun  30843  2ndresdju  30887  suppovss  30919  cosnop  30930  fpwrelmapffslem  30969  xaddeq0  30978  bcm1n  31018  divnumden2  31034  xmulcand  31097  xreceu  31098  s3f1  31123  ccatf1  31125  wrdt2ind  31127  swrdf1  31130  xrsmulgzz  31189  xrge0adddir  31203  xrge0adddi  31204  abliso  31207  gsumhashmul  31218  ogrpaddltrbid  31248  ogrpinvlt  31251  symgcom  31254  cyc2fv1  31290  cyc2fv2  31291  cycpmco2rn  31294  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2lem7  31301  cyc3fv1  31306  cyc3fv2  31307  cyc3fv3  31308  cycpmconjvlem  31310  cycpmconjslem2  31324  cycpmconjs  31325  cyc3conja  31326  archiabllem1a  31347  archiabllem1  31349  archiabllem2c  31351  slmdvs0  31380  dvrcan5  31392  ornglmullt  31408  orngrmullt  31409  rhmunitinv  31423  qusscaval  31454  imaslmod  31455  qustriv  31462  znfermltl  31464  quslsm  31495  nsgmgclem  31498  qsidomlem2  31531  mxidlprm  31542  ply1fermltl  31572  sradrng  31575  drgext0gsca  31581  rgmoddim  31595  matdim  31600  lbsdiflsp0  31609  dimkerim  31610  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  extdg1id  31640  ccfldextdgrr  31644  mdetpmtr2  31676  madjusmdetlem1  31679  mdetlap  31684  qtophaus  31688  zarcmplem  31733  qqhval2lem  31831  esumpad  31923  esummulc1  31949  esumsup  31957  measxun2  32078  measssd  32083  inelcarsg  32178  carsggect  32185  carsgclctunlem2  32186  pmeasmono  32191  oddpwdc  32221  eulerpartlemgs2  32247  eulerpartlemn  32248  totprobd  32293  signstfvn  32448  signstfveq0  32456  ftc2re  32478  itgexpif  32486  breprexpnat  32514  circlemethnat  32521  circlevma  32522  circlemethhgt  32523  hgt750lemf  32533  hgt750lemg  32534  hgt750lemb  32536  tgoldbachgt  32543  bnj1379  32710  bnj1321  32907  revpfxsfxrev  32977  revwlk  32986  subfaclim  33050  cvxsconn  33105  resconn  33108  cvmliftmolem1  33143  cvmliftlem7  33153  cvmliftlem13  33158  cvmlift2lem7  33171  cvmlift3lem5  33185  elmsta  33410  msubff1  33418  mthmpps  33444  bcm1nt  33609  faclim2  33620  funsseq  33648  nolesgn2o  33801  nolesgn2ores  33802  nogesgn1o  33803  nogesgn1ores  33804  nodenselem5  33818  nolt02o  33825  nogt01o  33826  nosupprefixmo  33830  noinfprefixmo  33831  sltlpss  34014  clsun  34444  topjoin  34481  bj-bary1lem  35408  irrdifflemf  35423  finxpreclem4  35492  matunitlindflem1  35700  ptrest  35703  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem9  35713  poimirlem11  35715  poimirlem12  35716  poimirlem26  35730  poimirlem27  35731  itg2addnclem  35755  itg2addnclem3  35757  itgaddnclem2  35763  itgsubnc  35766  iblmulc2nc  35769  itgabsnc  35773  ftc2nc  35786  areacirclem1  35792  areacirclem4  35795  areacirc  35797  cocanfo  35803  ablo4pnp  35965  rngolz  36007  rngorz  36008  zerdivemp1x  36032  crngm4  36088  crngohomfo  36091  lfl0  37006  lfladd  37007  lflmul  37009  eqlkr3  37042  olm11  37168  latm12  37171  cmtcomlemN  37189  omlspjN  37202  hlatj12  37312  1cvrjat  37416  dalemrotyz  37599  padd12N  37780  pmapjlln1  37796  atmod2i1  37802  pmapocjN  37871  pnonsingN  37874  pexmidN  37910  lhp2at0  37973  lhpelim  37978  ltrncnv  38087  cdleme7c  38186  cdleme15b  38216  cdlemednpq  38240  cdleme20m  38264  cdleme22cN  38283  cdleme22d  38284  cdleme23b  38291  cdleme30a  38319  cdleme35h  38397  cdlemeg46frv  38466  cdlemg2fv2  38541  cdlemg2l  38544  cdlemg2m  38545  cdlemg8c  38570  cdlemg10bALTN  38577  cdlemg12  38591  cdlemg13a  38592  cdlemg18c  38621  cdlemg19  38625  trlcoat  38664  cdlemg47  38677  tendo1ne0  38769  cdlemk9  38780  cdlemk9bN  38781  dia2dimlem1  39005  tendolinv  39046  tendorinv  39047  dvhlveclem  39049  doca3N  39068  dihmeetlem7N  39251  dihjatc1  39252  dihmeetlem18N  39265  dochnoncon  39332  dihjatc  39358  dihjatcclem1  39359  dihjatcclem4  39362  dochsnkr  39413  lcfl7lem  39440  lcfl8  39443  lcfl9a  39446  lclkrlem1  39447  lclkrlem2e  39452  lclkrlem2j  39457  lcfrlem1  39483  lcfrlem9  39491  lcfrlem23  39506  lcfrlem31  39514  mapd0  39606  mapdpglem21  39633  baerlem3lem1  39648  baerlem5alem1  39649  mapdindp4  39664  mapdh6gN  39683  hdmap1l6g  39757  hgmapval0  39833  hgmaprnlem1N  39837  hlhilhillem  39905  drngmulcanad  40178  drngmulcan2ad  40179  drnginvmuld  40180  pwsexpg  40193  mhphf  40208  sn-1ne2  40216  exp11d  40246  numdenexp  40258  resubeulem2  40280  resubidaddid1lem  40298  sn-00idlem1  40302  readdcan2  40316  sn-negex12  40319  sn-addcand  40322  remulinvcom  40335  remulid2  40336  remulcand  40341  sn-0tie0  40342  retire  40358  cnreeu  40359  prjspner1  40384  dffltz  40387  flt4lem5f  40410  flt4lem7  40412  fltnltalem  40415  fltnlta  40416  diophrw  40497  eldioph2lem1  40498  pellexlem2  40568  pellexlem6  40572  pellex  40573  pell1234qrne0  40591  pell1234qrreccl  40592  pell1qrgaplem  40611  rmxm1  40672  oddcomabszz  40682  jm2.19lem1  40727  jm3.1lem2  40756  dnnumch3  40788  pwssplit4  40830  flcidc  40915  deg1mhm  40948  sqrtcval  41138  radcnvrat  41821  nzprmdif  41826  hashnzfz  41827  dvsconst  41837  dvsid  41838  expgrowth  41842  bccm1k  41849  bccn1  41851  binomcxplemnotnn0  41863  subadd4b  42710  uzinico2  42990  sumnnodd  43061  limsupresuz  43134  limsupequzlem  43153  liminfresre  43210  liminfresuz  43215  climliminflimsupd  43232  icccncfext  43318  dvresntr  43349  itgsinexplem1  43385  itgsinexp  43386  stoweidlem1  43432  wallispi2lem2  43503  stirlinglem3  43507  stirlinglem5  43509  stirlinglem10  43514  stirlinglem15  43519  dirkertrigeqlem3  43531  dirkercncflem2  43535  fourierdlem26  43564  fourierdlem42  43580  fourierdlem66  43603  fourierdlem73  43610  fourierdlem81  43618  fourierdlem83  43620  fourierdlem107  43644  etransclem23  43688  meaiininclem  43914  vonvolmbl  44089  iccvonmbllem  44106  sigaradd  44269  cevathlem1  44270  imarnf1pr  44661  m1mod0mod1  44709  fmtnorec3  44888  proththd  44954  perfectALTVlem1  45061  perfectALTVlem2  45062  rnglz  45330  pw2m1lepw2m1  45749  nnpw2pmod  45817  dignn0flhalflem1  45849  affinecomb2  45937  1subrec1sub  45939  eenglngeehlnmlem1  45971  2itscplem3  46014  restcls2  46095  aacllem  46391  amgmlemALT  46393  young2d  46395