Theorem 3eqtr3d 2864

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  mpteqb  6787  fvmptt  6788  fvsnun2  6945  fsnunfv  6949  f1ocnvfv1  7033  f1ocnvfv2  7034  fcof1  7043  weniso  7107  caov12d  7369  caov13d  7371  caov411d  7373  caovmo  7385  onovuni  7979  tfrlem5  8016  seqomlem1  8086  seqomlem4  8089  onasuc  8153  onesuc  8155  oeeui  8228  fopwdom  8625  unxpdomlem2  8723  cantnfres  9140  cnfcom2lem  9164  cnfcom2  9165  updjud  9363  cardiun  9411  ackbij1lem16  9657  ackbij2lem2  9662  fpwwe2lem6  10057  fpwwe2lem8  10059  canthp1lem2  10075  mul12  10805  mul4  10808  addid1  10820  addcan  10824  addcom  10826  addcomd  10842  add12  10857  ppncan  10928  addsub4  10929  subeqxfrd  11049  subaddeqd  11055  muladd  11072  mulcand  11273  receu  11285  div13  11319  divdivdiv  11341  divcan5  11342  divdiv1  11351  divdiv2  11352  halfaddsub  11871  xadddi  12689  xov1plusxeqvd  12885  fztp  12964  flzadd  13197  fldiv  13229  mulp1mod1  13281  modnegd  13295  modsub12d  13297  2submod  13301  seqm1  13388  seqcaopr  13408  seqf1o  13412  exprec  13471  expsub  13478  zesq  13588  digit1  13599  discr1  13601  discr  13602  facnn2  13643  faclbnd6  13660  hashfz1  13707  hashdom  13741  hashun  13744  hashbclem  13811  hashfac  13817  seqcoll  13823  ccatopth  14078  repsw2  14312  repsw3  14313  shftval3  14435  crre  14473  resub  14486  imsub  14494  cjsub  14508  nn0sqeq1  14636  abslem2  14699  sqreulem  14719  bhmafibid1  14825  climshft2  14939  isercolllem2  15022  iseraltlem2  15039  iseraltlem3  15040  fsumsub  15143  telfsumo  15157  telfsumo2  15158  hashiun  15177  bcxmas  15190  climcndslem1  15204  climcndslem2  15205  trireciplem  15217  geoser  15222  geo2sum2  15230  fprodm1  15321  fallfacfwd  15390  binomfallfaclem2  15394  bpolydiflem  15408  bpoly4  15413  fsumcube  15414  sinsub  15521  cossub  15522  rpnnen2lem10  15576  ruclem12  15594  p1modz1  15614  mod2eq1n2dvds  15696  pwp1fsum  15742  divalglem9  15752  bitsinv1lem  15790  bitsinv1  15791  bitsf1  15795  sadasslem  15819  bitsres  15822  smup1  15838  smumul  15842  modgcd  15880  absmulgcd  15897  gcdmultiplezOLD  15901  eucalg  15931  lcmgcd  15951  lcmid  15953  lcmftp  15980  numdensq  16094  dfphi2  16111  phiprm  16114  fermltl  16121  prmdiveq  16123  hashgcdlem  16125  odzdvds  16132  powm2modprm  16140  modprm0  16142  coprimeprodsq  16145  pythagtriplem6  16158  pythagtriplem7  16159  pythagtriplem12  16163  pythagtriplem16  16167  pcaddlem  16224  sumhash  16232  pcfac  16235  pockthlem  16241  prmreclem6  16257  4sqlem12  16292  4sqlem15  16295  vdwlem3  16319  vdwlem6  16322  vdwlem9  16325  ramub1lem2  16363  cshwshashlem2  16430  qusaddvallem  16824  xpsaddlem  16846  xpsvsca  16850  mrcun  16893  homfeqval  16967  comfeqval  16978  sectcan  17025  sectco  17026  sectmon  17052  monsect  17053  funcsect  17142  setcmon  17347  resscatc  17365  catciso  17367  evlfcllem  17471  curf2cl  17481  curfcl  17482  yonedalem4c  17527  yonedalem3b  17529  yonedainv  17531  latj12  17706  grprinvlem  17883  grprinvd  17884  grpridd  17885  mnd12g  17924  resmhm  17985  pwsco2mhm  17997  frmdup3lem  18031  grprcan  18137  grplcan  18161  grpasscan1  18162  grpinv11  18168  grpinvnz  18170  grplmulf1o  18173  grpinvpropd  18174  grpinvadd  18177  grpsubsub4  18192  dfgrp3  18198  imasgrp2  18214  mhmid  18220  mhmmnd  18221  mulgz  18255  mulgdirlem  18258  mulgdir  18259  mulgass  18264  mulgsubdir  18267  mulgpropd  18269  pwsmulg  18272  isnsg3  18312  nmzsubg  18317  ssnmz  18318  eqger  18330  eqglact  18331  cyccom  18346  ghminv  18365  conjnmz  18392  subgga  18430  gasubg  18432  galcan  18434  gacan  18435  cntzsubg  18467  cntzmhm  18469  symgvalstruct  18525  psgnunilem2  18623  psgnuni  18627  sylow1lem1  18723  sylow2blem2  18746  sylow2blem3  18747  lsmmod  18801  lsmpropd  18803  lsmdisj2  18808  subgdisj1  18817  subgdisj2  18818  efgredleme  18869  efgredlemd  18870  efgredlemc  18871  efgredlem  18873  frgpup3lem  18903  mulgdi  18947  ghmcmn  18952  lsm4  18980  cygablOLD  19011  gsummhm2  19059  gsumpt  19082  gsum2d  19092  gsumcom3  19098  dprdfeq0  19144  ablfac1eu  19195  ablsimpgprmd  19237  ringcom  19329  isringd  19335  ringlz  19337  ringrz  19338  ring1eq0  19340  ringmneg1  19346  gsumdixp  19359  unitgrp  19417  irredrmul  19457  drngmul0or  19523  subrginv  19551  subrgunit  19553  primefld  19584  abvrec  19607  srngnvl  19627  srngadd  19628  srngmul  19629  issrngd  19632  lmodvs0  19668  lmodvneg1  19677  lmodcom  19680  lmodsubdi  19691  lmodvsinv  19808  lmodvsinv2  19809  lmhmvsca  19817  lvecvs0or  19880  lvecinv  19885  lspsnvs  19886  lspabs2  19892  lspfixed  19900  lspsolv  19915  unitrrg  20066  asclpropd  20126  psrass1lem  20157  psrlidm  20183  psrridm  20184  mvrf1  20205  mplmon2mul  20281  evlslem1  20295  evlseu  20296  evlssca  20302  evlsvar  20303  coe1pwmul  20447  pf1ind  20518  prmirredlem  20640  mulgrhm2  20646  chrrhm  20678  znidomb  20708  psgnghm  20724  psgninv  20726  zrhpsgnodpm  20736  evpmodpmf1o  20740  psgndiflemB  20744  ip0r  20781  ipdir  20783  ipdi  20784  ipass  20789  ipassr  20790  phlpropd  20799  ocvpj  20861  uvcresum  20937  lmimlbs  20980  mat0dimbas0  21075  mdetrlin  21211  mdetrsca  21212  mdetr0  21214  mdetunilem8  21228  mdetuni0  21230  mdetmul  21232  maducoeval2  21249  madurid  21253  madulid  21254  matinv  21286  matunit  21287  slesolinv  21289  slesolinvbi  21290  cpmadugsumlemF  21484  restin  21774  cncmp  22000  cmpsublem  22007  conndisj  22024  cnconn  22030  kgencmp2  22154  ufldom  22570  tgplacthmeo  22711  ghmcnp  22723  qustgpopn  22728  qustgphaus  22731  tsmsxplem2  22762  tususp  22881  xpsdsval  22991  blpnfctr  23046  xmssym  23075  ressxms  23135  isngp2  23206  ngppropd  23246  nminvr  23278  blcvx  23406  icccvx  23554  pcohtpylem  23623  pcohtpy  23624  clmvscom  23694  cvsmuleqdivd  23738  cvsdiveqd  23739  pjthlem1  24040  ovollb2lem  24089  ovolicc2lem1  24118  ovolicc2lem5  24122  volsup  24157  ovolioo  24169  uniiccdif  24179  uniioombllem3  24186  uniioombllem4  24187  vitalilem3  24211  itg1sub  24310  itg2const  24341  iblcnlem1  24388  itgcnlem  24390  itgaddlem2  24424  itgsub  24426  itgabs  24435  ditgsplit  24459  dvmulbr  24536  dvcmul  24541  dvcmulf  24542  dvrec  24552  dvmptres3  24553  dvmptadd  24557  dvmptmul  24558  dvmptres2  24559  dvmptneg  24563  dvmptsub  24564  dvmptcj  24565  dvmptco  24569  dveflem  24576  dvlip  24590  dvlipcn  24591  dvlip2  24592  dvcvx  24617  dvfsumle  24618  dvfsumabs  24620  dvfsumlem1  24623  dvfsumlem2  24624  ftc2  24641  ftc2ditglem  24642  itgparts  24644  itgsubstlem  24645  itgsubst  24646  fta1glem1  24759  fta1blem  24762  plyeq0lem  24800  plymullem1  24804  coeeulem  24814  coe0  24846  coesub  24847  dvply1  24873  plydivlem4  24885  plyrem  24894  fta1lem  24896  vieta1  24901  plyexmo  24902  elqaalem2  24909  aareccl  24915  aannenlem1  24917  aaliou3lem2  24932  dvtaylp  24958  taylthlem1  24961  radcnvlem1  25001  pserdvlem2  25016  efcvx  25037  ptolemy  25082  tangtx  25091  efif1olem3  25128  efif1olem4  25129  efabl  25134  lognegb  25173  efiarg  25190  cosargd  25191  tanarg  25202  logtayl  25243  cxpneg  25264  cxpsub  25265  cxprec  25269  cxproot  25273  cxpsqrt  25286  cxpcom  25320  cxpcn3lem  25328  cxpaddlelem  25332  abscxpbnd  25334  root1eq1  25336  cxpeq  25338  logrec  25341  isosctrlem2  25397  isosctrlem3  25398  isosctr  25399  ssscongptld  25400  chordthmlem  25410  heron  25416  quad2  25417  dcubic1lem  25421  mcubic  25425  cubic2  25426  cubic  25427  dquartlem2  25430  dquart  25431  quart1lem  25433  quart1  25434  asinlem2  25447  asinlem3  25449  asinsin  25470  sinacos  25483  atanlogsublem  25493  efiatan2  25495  2efiatan  25496  tanatan  25497  atantan  25501  atans2  25509  dvatan  25513  atantayl  25515  atantayl2  25516  log2cnv  25522  rlimcnp2  25544  cxplim  25549  cxp2lim  25554  cvxcl  25562  scvxcvx  25563  zetacvg  25592  lgamgulmlem4  25609  lgamcvg2  25632  gamp1  25635  wilthlem1  25645  wilthlem2  25646  ftalem5  25654  basellem3  25660  basellem5  25662  basellem8  25665  mumullem2  25757  musum  25768  musumsum  25769  muinv  25770  sgmppw  25773  1sgmprm  25775  1sgm2ppw  25776  ppiub  25780  logfac2  25793  chpchtsum  25795  perfectlem1  25805  perfectlem2  25806  dchrn0  25826  dchrfi  25831  dchrabs  25836  dchrptlem1  25840  dchrhash  25847  dchr2sum  25849  sum2dchr  25850  bposlem6  25865  bposlem9  25868  lgsvalmod  25892  lgsdilem  25900  lgsne0  25911  lgssq  25913  lgssq2  25914  lgsqr  25927  lgsdchrval  25930  lgsdchr  25931  gausslemma2dlem6  25948  gausslemma2d  25950  lgseisenlem1  25951  lgseisenlem2  25952  lgseisenlem4  25954  lgsquadlem1  25956  lgsquadlem3  25958  lgsquad3  25963  m1lgs  25964  2sqmod  26012  rplogsumlem1  26060  rplogsumlem2  26061  dchrisumlem2  26066  dchrisum0fno1  26087  rpvmasum2  26088  dchrisum0lem1  26092  dchrisum0lem2  26094  mudivsum  26106  mulog2sumlem1  26110  vmalogdivsum  26115  2vmadivsumlem  26116  logsqvma  26118  selberglem1  26121  selberglem2  26122  selberg2lem  26126  selberg3lem1  26133  selberg4lem1  26136  selberg4  26137  pntrsumo1  26141  selbergr  26144  selberg34r  26147  pntrlog2bndlem3  26155  pntrlog2bndlem4  26156  pntibndlem2  26167  pntlemg  26174  pntlemr  26178  pntlemf  26181  ostthlem1  26203  padicabvcxp  26208  ostth3  26214  tgcgrcomlr  26266  tgifscgr  26294  iscgrglt  26300  tgbtwnconn1lem2  26359  tgbtwnconn1lem3  26360  mirne  26453  miduniq2  26473  krippenlem  26476  ragcgr  26493  cgrg3col4  26639  f1otrg  26657  ttgcontlem1  26671  brbtwn2  26691  axsegconlem10  26712  ax5seglem3  26717  ax5seglem6  26720  axpaschlem  26726  axeuclidlem  26748  axcontlem2  26751  axcontlem7  26756  axcontlem8  26757  cusgrsizeindslem  27233  frgrncvvdeq  28088  numclwwlk7  28170  grpoidinvlem1  28281  grpoideu  28286  grporcan  28295  grpolcan  28307  grpoinvop  28310  ablo4  28327  nvscom  28406  nvmul0or  28427  nvz0  28445  smcnlem  28474  ipidsq  28487  sspz  28512  lno0  28533  lnoadd  28535  lnomul  28537  ipasslem3  28610  dipdi  28620  dipassr  28623  dipsubdi  28626  ubthlem2  28648  hvmul0or  28802  hvadd12  28812  hvadd4  28813  hvmulcom  28820  normneg  28921  pjhthlem1  29168  chj12  29311  spanunsni  29356  5oalem2  29432  3oalem2  29440  hoadd4  29561  homul12  29582  hosubdi  29585  honegsubdi  29587  hosub4  29590  adj2  29711  lnopmul  29744  lnopaddi  29748  lnfnaddi  29820  lnfnmuli  29821  cnlnadjlem6  29849  adjeq0  29868  leopmul  29911  opsqrlem1  29917  opsqrlem6  29922  hstnmoc  30000  strlem1  30027  chirredlem3  30169  reldisjun  30353  suppovss  30426  cosnop  30431  fpwrelmapffslem  30468  xaddeq0  30477  bcm1n  30518  divnumden2  30534  xmulcand  30597  xreceu  30598  s3f1  30623  ccatf1  30625  wrdt2ind  30627  swrdf1  30630  xrsmulgzz  30665  xrge0adddir  30679  xrge0adddi  30680  abliso  30683  ogrpaddltrbid  30721  ogrpinvlt  30724  symgcom  30727  cyc2fv1  30763  cyc2fv2  30764  cycpmco2rn  30767  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2lem7  30774  cyc3fv1  30779  cyc3fv2  30780  cyc3fv3  30781  cycpmconjvlem  30783  cycpmconjslem2  30797  cycpmconjs  30798  cyc3conja  30799  archiabllem1a  30820  archiabllem1  30822  archiabllem2c  30824  slmdvs0  30853  dvrcan5  30864  ornglmullt  30880  orngrmullt  30881  rhmunitinv  30895  qusscaval  30921  imaslmod  30922  qustriv  30929  qsidomlem2  30966  mxidlprm  30977  sradrng  30988  drgext0gsca  30994  rgmoddim  31008  matdim  31013  lbsdiflsp0  31022  dimkerim  31023  fedgmullem1  31025  fedgmullem2  31026  fedgmul  31027  extdg1id  31053  ccfldextdgrr  31057  mdetpmtr2  31089  madjusmdetlem1  31092  mdetlap  31097  qtophaus  31100  qqhval2lem  31222  esumpad  31314  esummulc1  31340  esumsup  31348  measxun2  31469  measssd  31474  inelcarsg  31569  carsggect  31576  carsgclctunlem2  31577  pmeasmono  31582  oddpwdc  31612  eulerpartlemgs2  31638  eulerpartlemn  31639  totprobd  31684  signstfvn  31839  signstfveq0  31847  ftc2re  31869  itgexpif  31877  breprexpnat  31905  circlemethnat  31912  circlevma  31913  circlemethhgt  31914  hgt750lemf  31924  hgt750lemg  31925  hgt750lemb  31927  tgoldbachgt  31934  bnj1379  32102  bnj1321  32299  revpfxsfxrev  32362  revwlk  32371  subfaclim  32435  cvxsconn  32490  resconn  32493  cvmliftmolem1  32528  cvmliftlem7  32538  cvmliftlem13  32543  cvmlift2lem7  32556  cvmlift3lem5  32570  elmsta  32795  msubff1  32803  mthmpps  32829  bcm1nt  32969  faclim2  32980  funsseq  33011  nolesgn2o  33178  nolesgn2ores  33179  nodenselem5  33192  nolt02o  33199  noprefixmo  33202  clsun  33676  topjoin  33713  bj-bary1lem  34594  bj-endbase  34600  bj-endcomp  34601  finxpreclem4  34678  matunitlindflem1  34903  ptrest  34906  poimirlem4  34911  poimirlem6  34913  poimirlem7  34914  poimirlem9  34916  poimirlem11  34918  poimirlem12  34919  poimirlem26  34933  poimirlem27  34934  itg2addnclem  34958  itg2addnclem3  34960  itgaddnclem2  34966  itgsubnc  34969  iblmulc2nc  34972  itgabsnc  34976  ftc2nc  34991  areacirclem1  34997  areacirclem4  35000  areacirc  35002  cocanfo  35008  ablo4pnp  35173  rngolz  35215  rngorz  35216  zerdivemp1x  35240  crngm4  35296  crngohomfo  35299  lfl0  36216  lfladd  36217  lflmul  36219  eqlkr3  36252  olm11  36378  latm12  36381  cmtcomlemN  36399  omlspjN  36412  hlatj12  36522  1cvrjat  36626  dalemrotyz  36809  padd12N  36990  pmapjlln1  37006  atmod2i1  37012  pmapocjN  37081  pnonsingN  37084  pexmidN  37120  lhp2at0  37183  lhpelim  37188  ltrncnv  37297  cdleme7c  37396  cdleme15b  37426  cdlemednpq  37450  cdleme20m  37474  cdleme22cN  37493  cdleme22d  37494  cdleme23b  37501  cdleme30a  37529  cdleme35h  37607  cdlemeg46frv  37676  cdlemg2fv2  37751  cdlemg2l  37754  cdlemg2m  37755  cdlemg8c  37780  cdlemg10bALTN  37787  cdlemg12  37801  cdlemg13a  37802  cdlemg18c  37831  cdlemg19  37835  trlcoat  37874  cdlemg47  37887  tendo1ne0  37979  cdlemk9  37990  cdlemk9bN  37991  dia2dimlem1  38215  tendolinv  38256  tendorinv  38257  dvhlveclem  38259  doca3N  38278  dihmeetlem7N  38461  dihjatc1  38462  dihmeetlem18N  38475  dochnoncon  38542  dihjatc  38568  dihjatcclem1  38569  dihjatcclem4  38572  dochsnkr  38623  lcfl7lem  38650  lcfl8  38653  lcfl9a  38656  lclkrlem1  38657  lclkrlem2e  38662  lclkrlem2j  38667  lcfrlem1  38693  lcfrlem9  38701  lcfrlem23  38716  lcfrlem31  38724  mapd0  38816  mapdpglem21  38843  baerlem3lem1  38858  baerlem5alem1  38859  mapdindp4  38874  mapdh6gN  38893  hdmap1l6g  38967  hgmapval0  39043  hgmaprnlem1N  39047  hlhilhillem  39111  sn-1ne2  39207  numdenexp  39235  exp11d  39238  resubeulem2  39255  resubidaddid1lem  39273  sn-00idlem1  39277  readdcan2  39291  remulinvcom  39297  remulid2  39298  remulcand  39299  dffltz  39320  fltnltalem  39323  fltnlta  39324  diophrw  39405  eldioph2lem1  39406  pellexlem2  39476  pellexlem6  39480  pellex  39481  pell1234qrne0  39499  pell1234qrreccl  39500  pell1qrgaplem  39519  rmxm1  39580  oddcomabszz  39590  jm2.19lem1  39635  jm3.1lem2  39664  dnnumch3  39696  pwssplit4  39738  flcidc  39823  deg1mhm  39856  itgpowd  39870  radcnvrat  40695  nzprmdif  40700  hashnzfz  40701  dvsconst  40711  dvsid  40712  expgrowth  40716  bccm1k  40723  bccn1  40725  binomcxplemnotnn0  40737  subadd4b  41597  uzinico2  41887  sumnnodd  41960  limsupresuz  42033  limsupequzlem  42052  liminfresre  42109  liminfresuz  42114  climliminflimsupd  42131  icccncfext  42219  dvresntr  42251  itgsinexplem1  42288  itgsinexp  42289  stoweidlem1  42335  wallispi2lem2  42406  stirlinglem3  42410  stirlinglem5  42412  stirlinglem10  42417  stirlinglem15  42422  dirkertrigeqlem3  42434  dirkercncflem2  42438  fourierdlem26  42467  fourierdlem42  42483  fourierdlem66  42506  fourierdlem73  42513  fourierdlem81  42521  fourierdlem83  42523  fourierdlem107  42547  etransclem23  42591  meaiininclem  42817  vonvolmbl  42992  iccvonmbllem  43009  sigaradd  43172  cevathlem1  43173  imarnf1pr  43530  m1mod0mod1  43578  fmtnorec3  43759  proththd  43828  perfectALTVlem1  43935  perfectALTVlem2  43936  rnglz  44204  pw2m1lepw2m1  44624  nnpw2pmod  44692  dignn0flhalflem1  44724  affinecomb2  44739  1subrec1sub  44741  eenglngeehlnmlem1  44773  2itscplem3  44816  aacllem  44951  amgmlemALT  44953  young2d  44955