Theorem 3eqtr3d 2839

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

Syntax hints:   → wi 4   = wceq 1522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788

This theorem is referenced by:  mpteqb  6653  fvmptt  6654  fvsnun2  6810  fsnunfv  6816  f1ocnvfv1  6898  f1ocnvfv2  6899  fcof1  6908  weniso  6970  caov12d  7225  caov13d  7227  caov411d  7229  caovmo  7241  grprinvlem  7242  grprinvd  7243  grpridd  7244  onovuni  7831  tfrlem5  7868  seqomlem1  7937  seqomlem4  7940  onasuc  8004  onesuc  8006  oeeui  8078  fopwdom  8472  unxpdomlem2  8569  cantnfres  8986  cnfcom2lem  9010  cnfcom2  9011  updjud  9209  cardiun  9257  ackbij1lem16  9503  ackbij2lem2  9508  fpwwe2lem6  9903  fpwwe2lem8  9905  canthp1lem2  9921  mul12  10652  mul4  10655  addid1  10667  addcan  10671  addcom  10673  addcomd  10689  add12  10704  ppncan  10776  addsub4  10777  subeqxfrd  10897  subaddeqd  10903  muladd  10920  mulcand  11121  receu  11133  div13  11167  divdivdiv  11189  divcan5  11190  divdiv1  11199  divdiv2  11200  halfaddsub  11718  xadddi  12538  xov1plusxeqvd  12734  fztp  12813  flzadd  13046  fldiv  13078  mulp1mod1  13130  modnegd  13144  modsub12d  13146  2submod  13150  seqm1  13237  seqcaopr  13257  seqf1o  13261  exprec  13320  expsub  13327  zesq  13437  digit1  13448  discr1  13450  discr  13451  facnn2  13492  faclbnd6  13509  hashfz1  13556  hashdom  13588  hashun  13591  hashbclem  13658  hashfac  13664  seqcoll  13670  ccatopth  13914  repsw2  14148  repsw3  14149  shftval3  14269  crre  14307  resub  14320  imsub  14328  cjsub  14342  nn0sqeq1  14470  abslem2  14533  sqreulem  14553  bhmafibid1  14659  climshft2  14773  isercolllem2  14856  iseraltlem2  14873  iseraltlem3  14874  fsumsub  14976  telfsumo  14990  telfsumo2  14991  hashiun  15010  bcxmas  15023  climcndslem1  15037  climcndslem2  15038  trireciplem  15050  geoser  15055  geo2sum2  15063  fprodm1  15154  fallfacfwd  15223  binomfallfaclem2  15227  bpolydiflem  15241  bpoly4  15246  fsumcube  15247  sinsub  15354  cossub  15355  rpnnen2lem10  15409  ruclem12  15427  p1modz1  15447  mod2eq1n2dvds  15529  pwp1fsum  15575  divalglem9  15585  bitsinv1lem  15623  bitsinv1  15624  bitsf1  15628  sadasslem  15652  bitsres  15655  smup1  15671  smumul  15675  modgcd  15713  absmulgcd  15726  gcdmultiplez  15730  eucalg  15760  lcmgcd  15780  lcmid  15782  lcmftp  15809  numdensq  15923  dfphi2  15940  phiprm  15943  fermltl  15950  prmdiveq  15952  hashgcdlem  15954  odzdvds  15961  powm2modprm  15969  modprm0  15971  coprimeprodsq  15974  pythagtriplem6  15987  pythagtriplem7  15988  pythagtriplem12  15992  pythagtriplem16  15996  pcaddlem  16053  sumhash  16061  pcfac  16064  pockthlem  16070  prmreclem6  16086  4sqlem12  16121  4sqlem15  16124  vdwlem3  16148  vdwlem6  16151  vdwlem9  16154  ramub1lem2  16192  cshwshashlem2  16259  qusaddvallem  16653  xpsaddlem  16675  xpsvsca  16679  mrcun  16722  homfeqval  16796  comfeqval  16807  sectcan  16854  sectco  16855  sectmon  16881  monsect  16882  funcsect  16971  setcmon  17176  resscatc  17194  catciso  17196  evlfcllem  17300  curf2cl  17310  curfcl  17311  yonedalem4c  17356  yonedalem3b  17358  yonedainv  17360  latj12  17535  mnd12g  17745  resmhm  17798  pwsco2mhm  17810  frmdup3lem  17842  grprcan  17894  grplcan  17918  grpasscan1  17919  grpinv11  17925  grpinvnz  17927  grplmulf1o  17930  grpinvpropd  17931  grpinvadd  17934  grpsubsub4  17949  dfgrp3  17955  imasgrp2  17971  mhmid  17977  mhmmnd  17978  mulgz  18009  mulgdirlem  18012  mulgdir  18013  mulgass  18018  mulgsubdir  18021  mulgpropd  18023  pwsmulg  18026  isnsg3  18067  nmzsubg  18074  ssnmz  18075  eqger  18083  eqglact  18084  ghminv  18106  conjnmz  18133  subgga  18171  gasubg  18173  galcan  18175  gacan  18176  cntzsubg  18208  cntzmhm  18210  psgnunilem2  18354  sylow1lem1  18453  sylow2blem2  18476  sylow2blem3  18477  lsmmod  18528  lsmpropd  18530  lsmdisj2  18535  subgdisj1  18544  subgdisj2  18545  efgredleme  18596  efgredlemd  18597  efgredlemc  18598  efgredlem  18600  frgpup3lem  18630  mulgdi  18672  ghmcmn  18677  lsm4  18703  cygabl  18732  gsummhm2  18779  gsumpt  18802  gsum2d  18812  dprdfeq0  18861  ablfac1eu  18912  ringcom  19019  isringd  19025  ringlz  19027  ringrz  19028  ring1eq0  19030  ringmneg1  19036  gsumdixp  19049  unitgrp  19107  irredrmul  19147  drngmul0or  19213  subrginv  19241  subrgunit  19243  primefld  19274  abvrec  19297  srngnvl  19317  srngadd  19318  srngmul  19319  issrngd  19322  lmodvs0  19358  lmodvneg1  19367  lmodcom  19370  lmodsubdi  19381  lmodvsinv  19498  lmodvsinv2  19499  lmhmvsca  19507  lvecvs0or  19570  lvecinv  19575  lspsnvs  19576  lspabs2  19582  lspfixed  19590  lspsolv  19605  unitrrg  19755  asclpropd  19814  psrass1lem  19845  psrlidm  19871  psrridm  19872  mvrf1  19893  mplmon2mul  19968  evlslem1  19982  evlseu  19983  evlssca  19989  evlsvar  19990  coe1pwmul  20130  pf1ind  20200  prmirredlem  20322  mulgrhm2  20328  chrrhm  20360  znidomb  20390  psgnghm  20406  psgninv  20408  zrhpsgnodpm  20418  evpmodpmf1o  20422  psgndiflemB  20426  ip0r  20463  ipdir  20465  ipdi  20466  ipass  20471  ipassr  20472  phlpropd  20481  ocvpj  20543  uvcresum  20619  lmimlbs  20662  gsumcom3  20692  mat0dimbas0  20759  mdetrlin  20895  mdetrsca  20896  mdetr0  20898  mdetunilem8  20912  mdetuni0  20914  mdetmul  20916  maducoeval2  20933  madurid  20937  madulid  20938  matinv  20970  matunit  20971  slesolinv  20973  slesolinvbi  20974  cpmadugsumlemF  21168  restin  21458  cncmp  21684  cmpsublem  21691  conndisj  21708  cnconn  21714  kgencmp2  21838  ufldom  22254  tgplacthmeo  22395  ghmcnp  22406  qustgpopn  22411  qustgphaus  22414  tsmsxplem2  22445  tususp  22564  xpsdsval  22674  blpnfctr  22729  xmssym  22758  ressxms  22818  isngp2  22889  ngppropd  22929  nminvr  22961  blcvx  23089  icccvx  23237  pcohtpylem  23306  pcohtpy  23307  clmvscom  23377  cvsmuleqdivd  23421  cvsdiveqd  23422  pjthlem1  23723  ovollb2lem  23772  ovolicc2lem1  23801  ovolicc2lem5  23805  volsup  23840  ovolioo  23852  uniiccdif  23862  uniioombllem3  23869  uniioombllem4  23870  vitalilem3  23894  itg1sub  23993  itg2const  24024  iblcnlem1  24071  itgcnlem  24073  itgaddlem2  24107  itgsub  24109  itgabs  24118  ditgsplit  24142  dvmulbr  24219  dvcmul  24224  dvcmulf  24225  dvrec  24235  dvmptres3  24236  dvmptadd  24240  dvmptmul  24241  dvmptres2  24242  dvmptneg  24246  dvmptsub  24247  dvmptcj  24248  dvmptco  24252  dveflem  24259  dvlip  24273  dvlipcn  24274  dvlip2  24275  dvcvx  24300  dvfsumle  24301  dvfsumabs  24303  dvfsumlem1  24306  dvfsumlem2  24307  ftc2  24324  ftc2ditglem  24325  itgparts  24327  itgsubstlem  24328  itgsubst  24329  fta1glem1  24442  fta1blem  24445  plyeq0lem  24483  plymullem1  24487  coeeulem  24497  coe0  24529  coesub  24530  dvply1  24556  plydivlem4  24568  plyrem  24577  fta1lem  24579  vieta1  24584  plyexmo  24585  elqaalem2  24592  aareccl  24598  aannenlem1  24600  aaliou3lem2  24615  dvtaylp  24641  taylthlem1  24644  radcnvlem1  24684  pserdvlem2  24699  efcvx  24720  ptolemy  24765  tangtx  24774  efif1olem3  24809  efif1olem4  24810  efabl  24815  lognegb  24854  efiarg  24871  cosargd  24872  tanarg  24883  logtayl  24924  cxpneg  24945  cxpsub  24946  cxprec  24950  cxproot  24954  cxpsqrt  24967  cxpcom  25001  cxpcn3lem  25009  cxpaddlelem  25013  abscxpbnd  25015  root1eq1  25017  cxpeq  25019  logrec  25022  isosctrlem2  25078  isosctrlem3  25079  isosctr  25080  ssscongptld  25081  chordthmlem  25091  heron  25097  quad2  25098  dcubic1lem  25102  mcubic  25106  cubic2  25107  cubic  25108  dquartlem2  25111  dquart  25112  quart1lem  25114  quart1  25115  asinlem2  25128  asinlem3  25130  asinsin  25151  sinacos  25164  atanlogsublem  25174  efiatan2  25176  2efiatan  25177  tanatan  25178  atantan  25182  atans2  25190  dvatan  25194  atantayl  25196  atantayl2  25197  log2cnv  25204  rlimcnp2  25226  cxplim  25231  cxp2lim  25236  cvxcl  25244  scvxcvx  25245  zetacvg  25274  lgamgulmlem4  25291  lgamcvg2  25314  gamp1  25317  wilthlem1  25327  wilthlem2  25328  ftalem5  25336  basellem3  25342  basellem5  25344  basellem8  25347  mumullem2  25439  musum  25450  musumsum  25451  muinv  25452  sgmppw  25455  1sgmprm  25457  1sgm2ppw  25458  ppiub  25462  logfac2  25475  chpchtsum  25477  perfectlem1  25487  perfectlem2  25488  dchrn0  25508  dchrfi  25513  dchrabs  25518  dchrptlem1  25522  dchrhash  25529  dchr2sum  25531  sum2dchr  25532  bposlem6  25547  bposlem9  25550  lgsvalmod  25574  lgsdilem  25582  lgsne0  25593  lgssq  25595  lgssq2  25596  lgsqr  25609  lgsdchrval  25612  lgsdchr  25613  gausslemma2dlem6  25630  gausslemma2d  25632  lgseisenlem1  25633  lgseisenlem2  25634  lgseisenlem4  25636  lgsquadlem1  25638  lgsquadlem3  25640  lgsquad3  25645  m1lgs  25646  2sqmod  25694  rplogsumlem1  25742  rplogsumlem2  25743  dchrisumlem2  25748  dchrisum0fno1  25769  rpvmasum2  25770  dchrisum0lem1  25774  dchrisum0lem2  25776  mudivsum  25788  mulog2sumlem1  25792  vmalogdivsum  25797  2vmadivsumlem  25798  logsqvma  25800  selberglem1  25803  selberglem2  25804  selberg2lem  25808  selberg3lem1  25815  selberg4lem1  25818  selberg4  25819  pntrsumo1  25823  selbergr  25826  selberg34r  25829  pntrlog2bndlem3  25837  pntrlog2bndlem4  25838  pntibndlem2  25849  pntlemg  25856  pntlemr  25860  pntlemf  25863  ostthlem1  25885  padicabvcxp  25890  ostth3  25896  tgcgrcomlr  25948  tgifscgr  25976  iscgrglt  25982  tgbtwnconn1lem2  26041  tgbtwnconn1lem3  26042  mirne  26135  miduniq2  26155  krippenlem  26158  ragcgr  26175  cgrg3col4  26322  f1otrg  26340  ttgcontlem1  26354  brbtwn2  26374  axsegconlem10  26395  ax5seglem3  26400  ax5seglem6  26403  axpaschlem  26409  axeuclidlem  26431  axcontlem2  26434  axcontlem7  26439  axcontlem8  26440  cusgrsizeindslem  26916  frgrncvvdeq  27780  numclwwlk7  27862  grpoidinvlem1  27972  grpoideu  27977  grporcan  27986  grpolcan  27998  grpoinvop  28001  ablo4  28018  nvscom  28097  nvmul0or  28118  nvz0  28136  smcnlem  28165  ipidsq  28178  sspz  28203  lno0  28224  lnoadd  28226  lnomul  28228  ipasslem3  28301  dipdi  28311  dipassr  28314  dipsubdi  28317  ubthlem2  28339  hvmul0or  28493  hvadd12  28503  hvadd4  28504  hvmulcom  28511  normneg  28612  pjhthlem1  28859  chj12  29002  spanunsni  29047  5oalem2  29123  3oalem2  29131  hoadd4  29252  homul12  29273  hosubdi  29276  honegsubdi  29278  hosub4  29281  adj2  29402  lnopmul  29435  lnopaddi  29439  lnfnaddi  29511  lnfnmuli  29512  cnlnadjlem6  29540  adjeq0  29559  leopmul  29602  opsqrlem1  29608  opsqrlem6  29613  hstnmoc  29691  strlem1  29718  chirredlem3  29860  reldisjun  30043  suppovss  30116  cosnop  30119  fpwrelmapffslem  30156  xaddeq0  30165  bcm1n  30204  divnumden2  30218  xmulcand  30281  xreceu  30282  s3f1  30303  wrdt2ind  30306  xrsmulgzz  30339  xrge0adddir  30353  xrge0adddi  30354  abliso  30357  ogrpaddltrbid  30381  ogrpinvlt  30384  symgcom  30386  cyc2fv1  30410  cyc2fv2  30411  cyc3fv1  30416  cyc3fv2  30417  cyc3fv3  30418  cycpmconjvlem  30420  cycpmconjslem2  30435  cycpmconjs  30436  cyc3conja  30437  archiabllem1a  30458  archiabllem1  30460  archiabllem2c  30462  slmdvs0  30491  dvrcan5  30518  ornglmullt  30534  orngrmullt  30535  rhmunitinv  30549  qusscaval  30575  imaslmod  30576  sradrng  30592  drgext0gsca  30598  rgmoddim  30612  matdim  30617  lbsdiflsp0  30626  dimkerim  30627  fedgmullem1  30629  fedgmullem2  30630  fedgmul  30631  extdg1id  30657  ccfldextdgrr  30661  mdetpmtr2  30704  madjusmdetlem1  30707  mdetlap  30712  qtophaus  30717  qqhval2lem  30839  esumpad  30931  esummulc1  30957  esumsup  30965  measxun2  31086  measssd  31091  inelcarsg  31186  carsggect  31193  carsgclctunlem2  31194  pmeasmono  31199  oddpwdc  31229  eulerpartlemgs2  31255  eulerpartlemn  31256  totprobd  31301  signstfvn  31456  signstfveq0  31464  ftc2re  31486  itgexpif  31494  breprexpnat  31522  circlemethnat  31529  circlevma  31530  circlemethhgt  31531  hgt750lemf  31541  hgt750lemg  31542  hgt750lemb  31544  tgoldbachgt  31551  bnj1379  31719  bnj1321  31913  subfaclim  32043  cvxsconn  32098  resconn  32101  cvmliftmolem1  32136  cvmliftlem7  32146  cvmliftlem13  32151  cvmlift2lem7  32164  cvmlift3lem5  32178  elmsta  32403  msubff1  32411  mthmpps  32437  bcm1nt  32577  faclim2  32588  funsseq  32619  nolesgn2o  32787  nolesgn2ores  32788  nodenselem5  32801  nolt02o  32808  noprefixmo  32811  clsun  33285  topjoin  33322  bj-bary1lem  34128  finxpreclem4  34206  matunitlindflem1  34419  ptrest  34422  poimirlem4  34427  poimirlem6  34429  poimirlem7  34430  poimirlem9  34432  poimirlem11  34434  poimirlem12  34435  poimirlem26  34449  poimirlem27  34450  itg2addnclem  34474  itg2addnclem3  34476  itgaddnclem2  34482  itgsubnc  34485  iblmulc2nc  34488  itgabsnc  34492  ftc2nc  34507  areacirclem1  34513  areacirclem4  34516  areacirc  34518  cocanfo  34525  ablo4pnp  34690  rngolz  34732  rngorz  34733  zerdivemp1x  34757  crngm4  34813  crngohomfo  34816  lfl0  35732  lfladd  35733  lflmul  35735  eqlkr3  35768  olm11  35894  latm12  35897  cmtcomlemN  35915  omlspjN  35928  hlatj12  36038  1cvrjat  36142  dalemrotyz  36325  padd12N  36506  pmapjlln1  36522  atmod2i1  36528  pmapocjN  36597  pnonsingN  36600  pexmidN  36636  lhp2at0  36699  lhpelim  36704  ltrncnv  36813  cdleme7c  36912  cdleme15b  36942  cdlemednpq  36966  cdleme20m  36990  cdleme22cN  37009  cdleme22d  37010  cdleme23b  37017  cdleme30a  37045  cdleme35h  37123  cdlemeg46frv  37192  cdlemg2fv2  37267  cdlemg2l  37270  cdlemg2m  37271  cdlemg8c  37296  cdlemg10bALTN  37303  cdlemg12  37317  cdlemg13a  37318  cdlemg18c  37347  cdlemg19  37351  trlcoat  37390  cdlemg47  37403  tendo1ne0  37495  cdlemk9  37506  cdlemk9bN  37507  dia2dimlem1  37731  tendolinv  37772  tendorinv  37773  dvhlveclem  37775  doca3N  37794  dihmeetlem7N  37977  dihjatc1  37978  dihmeetlem18N  37991  dochnoncon  38058  dihjatc  38084  dihjatcclem1  38085  dihjatcclem4  38088  dochsnkr  38139  lcfl7lem  38166  lcfl8  38169  lcfl9a  38172  lclkrlem1  38173  lclkrlem2e  38178  lclkrlem2j  38183  lcfrlem1  38209  lcfrlem9  38217  lcfrlem23  38232  lcfrlem31  38240  mapd0  38332  mapdpglem21  38359  baerlem3lem1  38374  baerlem5alem1  38375  mapdindp4  38390  mapdh6gN  38409  hdmap1l6g  38483  hgmapval0  38559  hgmaprnlem1N  38563  hlhilhillem  38627  ccatcan2d  38657  numdenexp  38708  exp11d  38711  resubeulem2  38729  resubidaddid1lem  38745  dffltz  38768  fltnltalem  38771  fltnlta  38772  diophrw  38841  eldioph2lem1  38842  pellexlem2  38912  pellexlem6  38916  pellex  38917  pell1234qrne0  38935  pell1234qrreccl  38936  pell1qrgaplem  38955  rmxm1  39016  oddcomabszz  39026  jm2.19lem1  39071  jm3.1lem2  39100  dnnumch3  39132  pwssplit4  39174  flcidc  39259  deg1mhm  39292  itgpowd  39306  ablsimpgprmd  40172  radcnvrat  40184  nzprmdif  40189  hashnzfz  40190  dvsconst  40200  dvsid  40201  expgrowth  40205  bccm1k  40212  bccn1  40214  binomcxplemnotnn0  40226  subadd4b  41089  uzinico2  41380  sumnnodd  41453  limsupresuz  41526  limsupequzlem  41545  liminfresre  41602  liminfresuz  41607  climliminflimsupd  41624  icccncfext  41711  dvresntr  41743  itgsinexplem1  41780  itgsinexp  41781  stoweidlem1  41828  wallispi2lem2  41899  stirlinglem3  41903  stirlinglem5  41905  stirlinglem10  41910  stirlinglem15  41915  dirkertrigeqlem3  41927  dirkercncflem2  41931  fourierdlem26  41960  fourierdlem42  41976  fourierdlem66  41999  fourierdlem73  42006  fourierdlem81  42014  fourierdlem83  42016  fourierdlem107  42040  etransclem23  42084  meaiininclem  42310  vonvolmbl  42485  iccvonmbllem  42502  sigaradd  42665  cevathlem1  42666  imarnf1pr  42997  m1mod0mod1  43045  fmtnorec3  43192  proththd  43261  perfectALTVlem1  43368  perfectALTVlem2  43369  rnglz  43633  pw2m1lepw2m1  44056  nnpw2pmod  44124  dignn0flhalflem1  44156  affinecomb2  44171  1subrec1sub  44173  eenglngeehlnmlem1  44205  2itscplem3  44248  aacllem  44382  amgmlemALT  44384  young2d  44386