Theorem 3eqtr3rd 2780

Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)

Hypotheses

Ref	Expression
3eqtr3d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3eqtr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3eqtr3rd	⊢ (𝜑 → 𝐷 = 𝐶)

Proof of Theorem 3eqtr3rd

Step	Hyp	Ref	Expression
1		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
2		3eqtr3d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3		3eqtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 3	eqtr3d 2773	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2773	1 ⊢ (𝜑 → 𝐷 = 𝐶)

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  iunxdif3  5037  fcofo  7243  fcof1oinvd  7248  cantnfp1lem3  9601  fin1a2lem7  10328  prlem934  10956  addlid  11329  addcom  11332  addcomd  11348  negeu  11383  add20  11662  2halves  12395  bcnn  14274  bcpasc  14283  hashfun  14399  hashf1dmrn  14405  wrdeqs1cat  14682  sqreulem  15322  summolem3  15676  fsumneg  15749  geolim  15835  geolim2  15836  mertens  15851  prodmolem3  15898  fallrisefac  15990  bpoly3  16023  sincossq  16143  demoivre  16167  eirrlem  16171  oddpwp1fsum  16361  sadeq  16441  gcdid  16496  gcdmultipled  16503  nn0rppwr  16530  phiprmpw  16746  pythagtriplem12  16797  expnprm  16873  fullresc  17818  grpinvid1  18967  grpnpcan  19008  grplactcnv  19019  ghmgrp  19042  conjghm  19224  odmodnn0  19515  gex1  19566  sylow3lem3  19604  efgredeu  19727  odadd2  19824  gsumval3  19882  pgpfac1lem3a  20053  omndmul2  20108  ringnegl  20283  ringnegr  20284  ringmneg2  20286  rdivmuldivd  20393  imadrhmcl  20774  lmodfopne  20895  lmodvsneg  20901  lssvs0or  21108  lvecinv  21111  lspabs2  21118  zringunit  21446  zringcyg  21449  dvdschrmulg  21508  fermltlchr  21509  sraassab  21848  mplcoe3  22016  mplcoe5  22018  evlvar  22086  psd1  22133  mdetrlin  22567  mdetunilem6  22582  cramerimplem3  22650  cramerimp  22651  paste  23259  tuslem  24231  tususs  24234  ngpds  24569  ioo2bl  24758  ipcau2  25201  dvexp3  25945  rolle  25957  cmvth  25958  dv11cn  25968  lhop  25983  itgsubstlem  26015  itgpowd  26017  ply1divex  26102  fta1glem1  26133  fta1g  26135  dgrnznn  26212  fta1  26274  vieta1lem2  26277  aaliou2  26306  dvtaylp  26335  dvntaylp  26336  taylthlem1  26338  taylthlem2  26339  dvradcnv  26386  ptolemy  26460  coskpi  26487  tanregt0  26503  cxpeq  26721  isosctrlem2  26783  chordthmlem  26796  dcubic  26810  quart1lem  26819  tanatan  26883  atantan  26887  dvatan  26899  birthdaylem2  26916  rlimcxp  26937  jensenlem2  26951  logdiflbnd  26958  emcllem2  26960  lgamgulmlem2  26993  lgamcvg2  27018  basellem8  27051  bclbnd  27243  lgsqr  27314  lgseisenlem3  27340  lgseisenlem4  27341  lgsquadlem1  27343  lgsquadlem2  27344  rpvmasumlem  27450  dchrisumlem1  27452  dchrisum0flblem1  27471  dchrisum0flblem2  27472  dchrisum0re  27476  dchrisum0lem1  27479  mudivsum  27493  mulogsum  27495  vmalogdivsum2  27501  logsqvma2  27506  selberg2lem  27513  logdivbnd  27519  selbergr  27531  selberg3r  27532  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntpbnd2  27550  pw2divscan4d  28436  pw2cutp1  28453  pw2cut2  28454  z12zsodd  28474  miduniq  28753  krippenlem  28758  colperpexlem2  28799  ttgcontlem1  28953  brbtwn2  28974  colinearalglem4  28978  axsegconlem9  28994  ax5seglem1  28997  axbtwnid  29008  axeuclidlem  29031  axcontlem2  29034  axcontlem4  29036  grpoinvid1  30599  vcz  30646  hosubsub4  31889  lnop0  32037  branmfn  32176  fressupp  32761  difico  32856  wrdsplex  32996  s3f1  33007  ccatf1  33009  mgcf1o  33063  mndlrinv  33084  cycpmco2lem4  33190  tocyccntz  33205  cyc3genpm  33213  cycpmconjslem2  33216  kerunit  33385  qustrivr  33425  znfermltl  33426  linds2eq  33441  dvdsruassoi  33444  dvdsruasso  33445  qsdrnglem2  33556  zringfrac  33614  m1pmeq  33645  vr1nz  33653  mplvrpmrhm  33691  esplyfval1  33717  ply1degltdimlem  33766  fedgmullem2  33774  fldextrspunlsplem  33817  constrrtll  33875  constrrtlc1  33876  constrrtcclem  33878  constrrtcc  33879  constrrecl  33913  2sqr3minply  33924  cos9thpiminplylem1  33926  cos9thpiminplylem2  33927  carsggect  34462  carsgclctunlem2  34463  ballotlemfrceq  34673  ballotlemrinv0  34677  hashreprin  34764  hgt750lemb  34800  faclimlem1  35925  irrdifflemf  37639  poimirlem4  37945  poimirlem23  37964  mblfinlem2  37979  voliunnfl  37985  volsupnfl  37986  itg2addnclem3  37994  ftc2nc  38023  dvasin  38025  areacirclem1  38029  areacirclem4  38032  rngonegmn1l  38262  rngonegmn1r  38263  lfl0  39511  latmassOLD  39675  omlmod1i2N  39706  llnexchb2lem  40314  dalawlem3  40319  pmapj2N  40375  osumcllem9N  40410  pexmidlem6N  40421  4atexlemc  40515  cdleme1  40673  cdleme42a  40917  cdlemg13a  41097  cdlemh2  41262  cdlemk1  41277  tendocnv  41467  dihmeetlem12N  41764  dihmeetlem16N  41768  dihmeetlem19N  41771  dochsatshp  41897  dochexmidlem6  41911  mapdval4N  42078  mapdpglem28  42147  mapdpglem31  42149  mapdindp4  42169  hdmap14lem1a  42312  hdmapinvlem4  42367  3rdpwhole  42724  oexpreposd  42754  remul01  42839  sn-negex12  42849  sn-subeu  42859  remulinvcom  42865  sn-0tie0  42896  cnreeu  42935  fltnlta  43096  irrapxlem5  43254  pellfund14  43326  rmxdbl  43367  jm2.22  43423  oaabsb  43722  oaun2  43809  oaun3  43810  sqrtcval  44068  0ellimcdiv  46077  fourierdlem95  46629  etransclem46  46708  sigariz  47291  sin5tlem2  47322  sin5tlem5  47325  cos5t  47327  ichreuopeq  47933  gricushgr  48393  altgsumbc  48828  blengt1fldiv2p1  49069  restclsseplem  49390  cofu1a  49569  cofu2a  49570  uobeqw  49694  swapf2fval  49740  swapf1val  49742  coccom  50139