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 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

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

This theorem is referenced by:  mpteqb  6782  fvmptt  6783  fvsnun2  6940  fsnunfv  6944  f1ocnvfv1  7027  f1ocnvfv2  7028  fcof1  7037  weniso  7101  caov12d  7363  caov13d  7365  caov411d  7367  caovmo  7379  onovuni  7973  tfrlem5  8010  seqomlem1  8080  seqomlem4  8083  onasuc  8147  onesuc  8149  oeeui  8222  fopwdom  8619  unxpdomlem2  8717  cantnfres  9134  cnfcom2lem  9158  cnfcom2  9159  updjud  9357  cardiun  9405  ackbij1lem16  9651  ackbij2lem2  9656  fpwwe2lem6  10051  fpwwe2lem8  10053  canthp1lem2  10069  mul12  10799  mul4  10802  addid1  10814  addcan  10818  addcom  10820  addcomd  10836  add12  10851  ppncan  10922  addsub4  10923  subeqxfrd  11043  subaddeqd  11049  muladd  11066  mulcand  11267  receu  11279  div13  11313  divdivdiv  11335  divcan5  11336  divdiv1  11345  divdiv2  11346  halfaddsub  11864  xadddi  12682  xov1plusxeqvd  12878  fztp  12957  flzadd  13190  fldiv  13222  mulp1mod1  13274  modnegd  13288  modsub12d  13290  2submod  13294  seqm1  13381  seqcaopr  13401  seqf1o  13405  exprec  13464  expsub  13471  zesq  13581  digit1  13592  discr1  13594  discr  13595  facnn2  13636  faclbnd6  13653  hashfz1  13700  hashdom  13734  hashun  13737  hashbclem  13804  hashfac  13810  seqcoll  13816  ccatopth  14072  repsw2  14306  repsw3  14307  shftval3  14429  crre  14467  resub  14480  imsub  14488  cjsub  14502  nn0sqeq1  14630  abslem2  14693  sqreulem  14713  bhmafibid1  14819  climshft2  14933  isercolllem2  15016  iseraltlem2  15033  iseraltlem3  15034  fsumsub  15137  telfsumo  15151  telfsumo2  15152  hashiun  15171  bcxmas  15184  climcndslem1  15198  climcndslem2  15199  trireciplem  15211  geoser  15216  geo2sum2  15224  fprodm1  15315  fallfacfwd  15384  binomfallfaclem2  15388  bpolydiflem  15402  bpoly4  15407  fsumcube  15408  sinsub  15515  cossub  15516  rpnnen2lem10  15570  ruclem12  15588  p1modz1  15608  mod2eq1n2dvds  15690  pwp1fsum  15736  divalglem9  15746  bitsinv1lem  15784  bitsinv1  15785  bitsf1  15789  sadasslem  15813  bitsres  15816  smup1  15832  smumul  15836  modgcd  15874  absmulgcd  15891  gcdmultiplezOLD  15895  eucalg  15925  lcmgcd  15945  lcmid  15947  lcmftp  15974  numdensq  16088  dfphi2  16105  phiprm  16108  fermltl  16115  prmdiveq  16117  hashgcdlem  16119  odzdvds  16126  powm2modprm  16134  modprm0  16136  coprimeprodsq  16139  pythagtriplem6  16152  pythagtriplem7  16153  pythagtriplem12  16157  pythagtriplem16  16161  pcaddlem  16218  sumhash  16226  pcfac  16229  pockthlem  16235  prmreclem6  16251  4sqlem12  16286  4sqlem15  16289  vdwlem3  16313  vdwlem6  16316  vdwlem9  16319  ramub1lem2  16357  cshwshashlem2  16424  qusaddvallem  16818  xpsaddlem  16840  xpsvsca  16844  mrcun  16887  homfeqval  16961  comfeqval  16972  sectcan  17019  sectco  17020  sectmon  17046  monsect  17047  funcsect  17136  setcmon  17341  resscatc  17359  catciso  17361  evlfcllem  17465  curf2cl  17475  curfcl  17476  yonedalem4c  17521  yonedalem3b  17523  yonedainv  17525  latj12  17700  grprinvlem  17877  grprinvd  17878  grpridd  17879  mnd12g  17918  resmhm  17979  pwsco2mhm  17991  frmdup3lem  18025  grprcan  18131  grplcan  18155  grpasscan1  18156  grpinv11  18162  grpinvnz  18164  grplmulf1o  18167  grpinvpropd  18168  grpinvadd  18171  grpsubsub4  18186  dfgrp3  18192  imasgrp2  18208  mhmid  18214  mhmmnd  18215  mulgz  18249  mulgdirlem  18252  mulgdir  18253  mulgass  18258  mulgsubdir  18261  mulgpropd  18263  pwsmulg  18266  isnsg3  18306  nmzsubg  18311  ssnmz  18312  eqger  18324  eqglact  18325  cyccom  18340  ghminv  18359  conjnmz  18386  subgga  18424  gasubg  18426  galcan  18428  gacan  18429  cntzsubg  18461  cntzmhm  18463  symgvalstruct  18519  psgnunilem2  18617  psgnuni  18621  sylow1lem1  18717  sylow2blem2  18740  sylow2blem3  18741  lsmmod  18795  lsmpropd  18797  lsmdisj2  18802  subgdisj1  18811  subgdisj2  18812  efgredleme  18863  efgredlemd  18864  efgredlemc  18865  efgredlem  18867  frgpup3lem  18897  mulgdi  18941  ghmcmn  18946  lsm4  18974  cygablOLD  19005  gsummhm2  19053  gsumpt  19076  gsum2d  19086  gsumcom3  19092  dprdfeq0  19138  ablfac1eu  19189  ablsimpgprmd  19231  ringcom  19323  isringd  19329  ringlz  19331  ringrz  19332  ring1eq0  19334  ringmneg1  19340  gsumdixp  19353  unitgrp  19411  irredrmul  19451  drngmul0or  19517  subrginv  19545  subrgunit  19547  primefld  19578  abvrec  19601  srngnvl  19621  srngadd  19622  srngmul  19623  issrngd  19626  lmodvs0  19662  lmodvneg1  19671  lmodcom  19674  lmodsubdi  19685  lmodvsinv  19802  lmodvsinv2  19803  lmhmvsca  19811  lvecvs0or  19874  lvecinv  19879  lspsnvs  19880  lspabs2  19886  lspfixed  19894  lspsolv  19909  unitrrg  20060  asclpropd  20120  psrass1lem  20151  psrlidm  20177  psrridm  20178  mvrf1  20199  mplmon2mul  20275  evlslem1  20289  evlseu  20290  evlssca  20296  evlsvar  20297  coe1pwmul  20441  pf1ind  20512  prmirredlem  20634  mulgrhm2  20640  chrrhm  20672  znidomb  20702  psgnghm  20718  psgninv  20720  zrhpsgnodpm  20730  evpmodpmf1o  20734  psgndiflemB  20738  ip0r  20775  ipdir  20777  ipdi  20778  ipass  20783  ipassr  20784  phlpropd  20793  ocvpj  20855  uvcresum  20931  lmimlbs  20974  mat0dimbas0  21069  mdetrlin  21205  mdetrsca  21206  mdetr0  21208  mdetunilem8  21222  mdetuni0  21224  mdetmul  21226  maducoeval2  21243  madurid  21247  madulid  21248  matinv  21280  matunit  21281  slesolinv  21283  slesolinvbi  21284  cpmadugsumlemF  21478  restin  21768  cncmp  21994  cmpsublem  22001  conndisj  22018  cnconn  22024  kgencmp2  22148  ufldom  22564  tgplacthmeo  22705  ghmcnp  22717  qustgpopn  22722  qustgphaus  22725  tsmsxplem2  22756  tususp  22875  xpsdsval  22985  blpnfctr  23040  xmssym  23069  ressxms  23129  isngp2  23200  ngppropd  23240  nminvr  23272  blcvx  23400  icccvx  23548  pcohtpylem  23617  pcohtpy  23618  clmvscom  23688  cvsmuleqdivd  23732  cvsdiveqd  23733  pjthlem1  24034  ovollb2lem  24083  ovolicc2lem1  24112  ovolicc2lem5  24116  volsup  24151  ovolioo  24163  uniiccdif  24173  uniioombllem3  24180  uniioombllem4  24181  vitalilem3  24205  itg1sub  24304  itg2const  24335  iblcnlem1  24382  itgcnlem  24384  itgaddlem2  24418  itgsub  24420  itgabs  24429  ditgsplit  24453  dvmulbr  24530  dvcmul  24535  dvcmulf  24536  dvrec  24546  dvmptres3  24547  dvmptadd  24551  dvmptmul  24552  dvmptres2  24553  dvmptneg  24557  dvmptsub  24558  dvmptcj  24559  dvmptco  24563  dveflem  24570  dvlip  24584  dvlipcn  24585  dvlip2  24586  dvcvx  24611  dvfsumle  24612  dvfsumabs  24614  dvfsumlem1  24617  dvfsumlem2  24618  ftc2  24635  ftc2ditglem  24636  itgparts  24638  itgsubstlem  24639  itgsubst  24640  fta1glem1  24753  fta1blem  24756  plyeq0lem  24794  plymullem1  24798  coeeulem  24808  coe0  24840  coesub  24841  dvply1  24867  plydivlem4  24879  plyrem  24888  fta1lem  24890  vieta1  24895  plyexmo  24896  elqaalem2  24903  aareccl  24909  aannenlem1  24911  aaliou3lem2  24926  dvtaylp  24952  taylthlem1  24955  radcnvlem1  24995  pserdvlem2  25010  efcvx  25031  ptolemy  25076  tangtx  25085  efif1olem3  25122  efif1olem4  25123  efabl  25128  lognegb  25167  efiarg  25184  cosargd  25185  tanarg  25196  logtayl  25237  cxpneg  25258  cxpsub  25259  cxprec  25263  cxproot  25267  cxpsqrt  25280  cxpcom  25314  cxpcn3lem  25322  cxpaddlelem  25326  abscxpbnd  25328  root1eq1  25330  cxpeq  25332  logrec  25335  isosctrlem2  25391  isosctrlem3  25392  isosctr  25393  ssscongptld  25394  chordthmlem  25404  heron  25410  quad2  25411  dcubic1lem  25415  mcubic  25419  cubic2  25420  cubic  25421  dquartlem2  25424  dquart  25425  quart1lem  25427  quart1  25428  asinlem2  25441  asinlem3  25443  asinsin  25464  sinacos  25477  atanlogsublem  25487  efiatan2  25489  2efiatan  25490  tanatan  25491  atantan  25495  atans2  25503  dvatan  25507  atantayl  25509  atantayl2  25510  log2cnv  25516  rlimcnp2  25538  cxplim  25543  cxp2lim  25548  cvxcl  25556  scvxcvx  25557  zetacvg  25586  lgamgulmlem4  25603  lgamcvg2  25626  gamp1  25629  wilthlem1  25639  wilthlem2  25640  ftalem5  25648  basellem3  25654  basellem5  25656  basellem8  25659  mumullem2  25751  musum  25762  musumsum  25763  muinv  25764  sgmppw  25767  1sgmprm  25769  1sgm2ppw  25770  ppiub  25774  logfac2  25787  chpchtsum  25789  perfectlem1  25799  perfectlem2  25800  dchrn0  25820  dchrfi  25825  dchrabs  25830  dchrptlem1  25834  dchrhash  25841  dchr2sum  25843  sum2dchr  25844  bposlem6  25859  bposlem9  25862  lgsvalmod  25886  lgsdilem  25894  lgsne0  25905  lgssq  25907  lgssq2  25908  lgsqr  25921  lgsdchrval  25924  lgsdchr  25925  gausslemma2dlem6  25942  gausslemma2d  25944  lgseisenlem1  25945  lgseisenlem2  25946  lgseisenlem4  25948  lgsquadlem1  25950  lgsquadlem3  25952  lgsquad3  25957  m1lgs  25958  2sqmod  26006  rplogsumlem1  26054  rplogsumlem2  26055  dchrisumlem2  26060  dchrisum0fno1  26081  rpvmasum2  26082  dchrisum0lem1  26086  dchrisum0lem2  26088  mudivsum  26100  mulog2sumlem1  26104  vmalogdivsum  26109  2vmadivsumlem  26110  logsqvma  26112  selberglem1  26115  selberglem2  26116  selberg2lem  26120  selberg3lem1  26127  selberg4lem1  26130  selberg4  26131  pntrsumo1  26135  selbergr  26138  selberg34r  26141  pntrlog2bndlem3  26149  pntrlog2bndlem4  26150  pntibndlem2  26161  pntlemg  26168  pntlemr  26172  pntlemf  26175  ostthlem1  26197  padicabvcxp  26202  ostth3  26208  tgcgrcomlr  26260  tgifscgr  26288  iscgrglt  26294  tgbtwnconn1lem2  26353  tgbtwnconn1lem3  26354  mirne  26447  miduniq2  26467  krippenlem  26470  ragcgr  26487  cgrg3col4  26633  f1otrg  26651  ttgcontlem1  26665  brbtwn2  26685  axsegconlem10  26706  ax5seglem3  26711  ax5seglem6  26714  axpaschlem  26720  axeuclidlem  26742  axcontlem2  26745  axcontlem7  26750  axcontlem8  26751  cusgrsizeindslem  27227  frgrncvvdeq  28082  numclwwlk7  28164  grpoidinvlem1  28275  grpoideu  28280  grporcan  28289  grpolcan  28301  grpoinvop  28304  ablo4  28321  nvscom  28400  nvmul0or  28421  nvz0  28439  smcnlem  28468  ipidsq  28481  sspz  28506  lno0  28527  lnoadd  28529  lnomul  28531  ipasslem3  28604  dipdi  28614  dipassr  28617  dipsubdi  28620  ubthlem2  28642  hvmul0or  28796  hvadd12  28806  hvadd4  28807  hvmulcom  28814  normneg  28915  pjhthlem1  29162  chj12  29305  spanunsni  29350  5oalem2  29426  3oalem2  29434  hoadd4  29555  homul12  29576  hosubdi  29579  honegsubdi  29581  hosub4  29584  adj2  29705  lnopmul  29738  lnopaddi  29742  lnfnaddi  29814  lnfnmuli  29815  cnlnadjlem6  29843  adjeq0  29862  leopmul  29905  opsqrlem1  29911  opsqrlem6  29916  hstnmoc  29994  strlem1  30021  chirredlem3  30163  reldisjun  30347  suppovss  30420  cosnop  30425  fpwrelmapffslem  30462  xaddeq0  30471  bcm1n  30512  divnumden2  30528  xmulcand  30592  xreceu  30593  s3f1  30618  ccatf1  30620  wrdt2ind  30622  swrdf1  30625  xrsmulgzz  30660  xrge0adddir  30674  xrge0adddi  30675  abliso  30678  ogrpaddltrbid  30716  ogrpinvlt  30719  symgcom  30722  cyc2fv1  30758  cyc2fv2  30759  cycpmco2rn  30762  cycpmco2lem5  30767  cycpmco2lem6  30768  cycpmco2lem7  30769  cyc3fv1  30774  cyc3fv2  30775  cyc3fv3  30776  cycpmconjvlem  30778  cycpmconjslem2  30792  cycpmconjs  30793  cyc3conja  30794  archiabllem1a  30815  archiabllem1  30817  archiabllem2c  30819  slmdvs0  30848  dvrcan5  30859  ornglmullt  30875  orngrmullt  30876  rhmunitinv  30890  qusscaval  30916  imaslmod  30917  qustriv  30924  qsidomlem2  30961  mxidlprm  30972  sradrng  30983  drgext0gsca  30989  rgmoddim  31003  matdim  31008  lbsdiflsp0  31017  dimkerim  31018  fedgmullem1  31020  fedgmullem2  31021  fedgmul  31022  extdg1id  31048  ccfldextdgrr  31052  mdetpmtr2  31084  madjusmdetlem1  31087  mdetlap  31092  qtophaus  31095  qqhval2lem  31217  esumpad  31309  esummulc1  31335  esumsup  31343  measxun2  31464  measssd  31469  inelcarsg  31564  carsggect  31571  carsgclctunlem2  31572  pmeasmono  31577  oddpwdc  31607  eulerpartlemgs2  31633  eulerpartlemn  31634  totprobd  31679  signstfvn  31834  signstfveq0  31842  ftc2re  31864  itgexpif  31872  breprexpnat  31900  circlemethnat  31907  circlevma  31908  circlemethhgt  31909  hgt750lemf  31919  hgt750lemg  31920  hgt750lemb  31922  tgoldbachgt  31929  bnj1379  32097  bnj1321  32294  revpfxsfxrev  32357  revwlk  32366  subfaclim  32430  cvxsconn  32485  resconn  32488  cvmliftmolem1  32523  cvmliftlem7  32533  cvmliftlem13  32538  cvmlift2lem7  32551  cvmlift3lem5  32565  elmsta  32790  msubff1  32798  mthmpps  32824  bcm1nt  32964  faclim2  32975  funsseq  33006  nolesgn2o  33173  nolesgn2ores  33174  nodenselem5  33187  nolt02o  33194  noprefixmo  33197  clsun  33671  topjoin  33708  bj-bary1lem  34585  bj-endbase  34591  bj-endcomp  34592  finxpreclem4  34669  matunitlindflem1  34882  ptrest  34885  poimirlem4  34890  poimirlem6  34892  poimirlem7  34893  poimirlem9  34895  poimirlem11  34897  poimirlem12  34898  poimirlem26  34912  poimirlem27  34913  itg2addnclem  34937  itg2addnclem3  34939  itgaddnclem2  34945  itgsubnc  34948  iblmulc2nc  34951  itgabsnc  34955  ftc2nc  34970  areacirclem1  34976  areacirclem4  34979  areacirc  34981  cocanfo  34987  ablo4pnp  35152  rngolz  35194  rngorz  35195  zerdivemp1x  35219  crngm4  35275  crngohomfo  35278  lfl0  36195  lfladd  36196  lflmul  36198  eqlkr3  36231  olm11  36357  latm12  36360  cmtcomlemN  36378  omlspjN  36391  hlatj12  36501  1cvrjat  36605  dalemrotyz  36788  padd12N  36969  pmapjlln1  36985  atmod2i1  36991  pmapocjN  37060  pnonsingN  37063  pexmidN  37099  lhp2at0  37162  lhpelim  37167  ltrncnv  37276  cdleme7c  37375  cdleme15b  37405  cdlemednpq  37429  cdleme20m  37453  cdleme22cN  37472  cdleme22d  37473  cdleme23b  37480  cdleme30a  37508  cdleme35h  37586  cdlemeg46frv  37655  cdlemg2fv2  37730  cdlemg2l  37733  cdlemg2m  37734  cdlemg8c  37759  cdlemg10bALTN  37766  cdlemg12  37780  cdlemg13a  37781  cdlemg18c  37810  cdlemg19  37814  trlcoat  37853  cdlemg47  37866  tendo1ne0  37958  cdlemk9  37969  cdlemk9bN  37970  dia2dimlem1  38194  tendolinv  38235  tendorinv  38236  dvhlveclem  38238  doca3N  38257  dihmeetlem7N  38440  dihjatc1  38441  dihmeetlem18N  38454  dochnoncon  38521  dihjatc  38547  dihjatcclem1  38548  dihjatcclem4  38551  dochsnkr  38602  lcfl7lem  38629  lcfl8  38632  lcfl9a  38635  lclkrlem1  38636  lclkrlem2e  38641  lclkrlem2j  38646  lcfrlem1  38672  lcfrlem9  38680  lcfrlem23  38695  lcfrlem31  38703  mapd0  38795  mapdpglem21  38822  baerlem3lem1  38837  baerlem5alem1  38838  mapdindp4  38853  mapdh6gN  38872  hdmap1l6g  38946  hgmapval0  39022  hgmaprnlem1N  39026  hlhilhillem  39090  sn-1ne2  39151  numdenexp  39179  exp11d  39182  resubeulem2  39199  resubidaddid1lem  39217  sn-00idlem1  39221  readdcan2  39235  remulinvcom  39241  remulid2  39242  remulcand  39243  dffltz  39264  fltnltalem  39267  fltnlta  39268  diophrw  39349  eldioph2lem1  39350  pellexlem2  39420  pellexlem6  39424  pellex  39425  pell1234qrne0  39443  pell1234qrreccl  39444  pell1qrgaplem  39463  rmxm1  39524  oddcomabszz  39534  jm2.19lem1  39579  jm3.1lem2  39608  dnnumch3  39640  pwssplit4  39682  flcidc  39767  deg1mhm  39800  itgpowd  39814  radcnvrat  40639  nzprmdif  40644  hashnzfz  40645  dvsconst  40655  dvsid  40656  expgrowth  40660  bccm1k  40667  bccn1  40669  binomcxplemnotnn0  40681  subadd4b  41540  uzinico2  41830  sumnnodd  41903  limsupresuz  41976  limsupequzlem  41995  liminfresre  42052  liminfresuz  42057  climliminflimsupd  42074  icccncfext  42162  dvresntr  42194  itgsinexplem1  42231  itgsinexp  42232  stoweidlem1  42279  wallispi2lem2  42350  stirlinglem3  42354  stirlinglem5  42356  stirlinglem10  42361  stirlinglem15  42366  dirkertrigeqlem3  42378  dirkercncflem2  42382  fourierdlem26  42411  fourierdlem42  42427  fourierdlem66  42450  fourierdlem73  42457  fourierdlem81  42465  fourierdlem83  42467  fourierdlem107  42491  etransclem23  42535  meaiininclem  42761  vonvolmbl  42936  iccvonmbllem  42953  sigaradd  43116  cevathlem1  43117  imarnf1pr  43474  m1mod0mod1  43522  fmtnorec3  43703  proththd  43772  perfectALTVlem1  43879  perfectALTVlem2  43880  rnglz  44148  pw2m1lepw2m1  44568  nnpw2pmod  44636  dignn0flhalflem1  44668  affinecomb2  44683  1subrec1sub  44685  eenglngeehlnmlem1  44717  2itscplem3  44760  aacllem  44895  amgmlemALT  44897  young2d  44899