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 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728

This theorem is referenced by:  iunxdif3  4989  fcofo  7076  fcof1oinvd  7081  cantnfp1lem3  9273  fin1a2lem7  9985  prlem934  10612  addid2  10980  addcom  10983  addcomd  10999  negeu  11033  add20  11309  2halves  12023  bcnn  13843  bcpasc  13852  hashfun  13969  wrdeqs1cat  14250  sqreulem  14888  summolem3  15243  fsumneg  15314  geolim  15397  geolim2  15398  mertens  15413  prodmolem3  15458  fallrisefac  15550  bpoly3  15583  sincossq  15700  demoivre  15724  eirrlem  15728  oddpwp1fsum  15916  sadeq  15994  gcdid  16049  gcdmultipled  16057  phiprmpw  16292  pythagtriplem12  16342  expnprm  16418  fullresc  17311  grpinvid1  18372  grpnpcan  18409  grplactcnv  18420  ghmgrp  18441  conjghm  18607  odmodnn0  18886  gex1  18934  sylow3lem3  18972  efgredeu  19096  odadd2  19188  gsumval3  19246  pgpfac1lem3a  19417  ringnegl  19566  rngnegr  19567  ringmneg2  19569  lmodfopne  19891  lmodvsneg  19897  lss0v  20007  lssvs0or  20101  lvecinv  20104  lspabs2  20111  zringunit  20407  zringcyg  20410  mplcoe3  20949  mplcoe5  20951  evlvar  21014  mdetrlin  21453  mdetunilem6  21468  cramerimplem3  21536  cramerimp  21537  paste  22145  tuslem  23118  tususs  23121  ngpds  23456  ioo2bl  23644  ipcau2  24085  dvexp3  24829  rolle  24841  cmvth  24842  dv11cn  24852  lhop  24867  itgsubstlem  24899  itgpowd  24901  ply1divex  24988  fta1glem1  25017  fta1g  25019  dgrnznn  25095  fta1  25155  vieta1lem2  25158  aaliou2  25187  dvtaylp  25216  dvntaylp  25217  taylthlem1  25219  taylthlem2  25220  dvradcnv  25267  ptolemy  25340  coskpi  25366  tanregt0  25382  cxpeq  25597  isosctrlem2  25656  chordthmlem  25669  dcubic  25683  quart1lem  25692  tanatan  25756  atantan  25760  dvatan  25772  birthdaylem2  25789  rlimcxp  25810  jensenlem2  25824  logdiflbnd  25831  emcllem2  25833  lgamgulmlem2  25866  lgamcvg2  25891  basellem8  25924  bclbnd  26115  lgsqr  26186  lgseisenlem3  26212  lgseisenlem4  26213  lgsquadlem1  26215  lgsquadlem2  26216  rpvmasumlem  26322  dchrisumlem1  26324  dchrisum0flblem1  26343  dchrisum0flblem2  26344  dchrisum0re  26348  dchrisum0lem1  26351  mudivsum  26365  mulogsum  26367  vmalogdivsum2  26373  logsqvma2  26378  selberg2lem  26385  logdivbnd  26391  selbergr  26403  selberg3r  26404  pntrlog2bndlem4  26415  pntrlog2bndlem5  26416  pntpbnd2  26422  miduniq  26730  krippenlem  26735  colperpexlem2  26776  ttgcontlem1  26930  brbtwn2  26950  colinearalglem4  26954  axsegconlem9  26970  ax5seglem1  26973  axbtwnid  26984  axeuclidlem  27007  axcontlem2  27010  axcontlem4  27012  grpoinvid1  28563  vcz  28610  hosubsub4  29853  lnop0  30001  branmfn  30140  fressupp  30696  difico  30778  wrdsplex  30886  s3f1  30895  ccatf1  30897  mgcf1o  30954  omndmul2  31011  cycpmco2lem4  31069  tocyccntz  31084  cyc3genpm  31092  cycpmconjslem2  31095  dvdschrmulg  31156  rdivmuldivd  31161  kerunit  31195  qustrivr  31229  znfermltl  31230  linds2eq  31243  fedgmullem2  31379  carsggect  31951  carsgclctunlem2  31952  ballotlemfrceq  32161  ballotlemrinv0  32165  hashreprin  32266  hgt750lemb  32302  hashf1dmrn  32742  faclimlem1  33378  irrdifflemf  35179  poimirlem4  35467  poimirlem23  35486  mblfinlem2  35501  voliunnfl  35507  volsupnfl  35508  itg2addnclem3  35516  ftc2nc  35545  dvasin  35547  areacirclem1  35551  areacirclem4  35554  rngonegmn1l  35785  rngonegmn1r  35786  lfl0  36765  latmassOLD  36929  omlmod1i2N  36960  llnexchb2lem  37568  dalawlem3  37573  pmapj2N  37629  osumcllem9N  37664  pexmidlem6N  37675  4atexlemc  37769  cdleme1  37927  cdleme42a  38171  cdlemg13a  38351  cdlemh2  38516  cdlemk1  38531  tendocnv  38721  dihmeetlem12N  39018  dihmeetlem16N  39022  dihmeetlem19N  39025  dochsatshp  39151  dochexmidlem6  39165  mapdval4N  39332  mapdpglem28  39401  mapdpglem31  39403  mapdindp4  39423  hdmap14lem1a  39566  hdmapinvlem4  39621  oexpreposd  39969  nn0rppwr  39982  sn-00idlem3  40032  remul01  40039  sn-subeu  40057  remulinvcom  40063  sn-0tie0  40070  cnreeu  40087  fltnlta  40144  irrapxlem5  40292  pellfund14  40364  rmxdbl  40405  jm2.22  40461  sqrtcval  40866  0ellimcdiv  42808  fourierdlem95  43360  etransclem46  43439  sigariz  43994  ichreuopeq  44541  isomushgr  44894  altgsumbc  45304  blengt1fldiv2p1  45555  restclsseplem  45824