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 1541

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  iunxdif3  5060  fcofo  7239  fcof1oinvd  7244  cantnfp1lem3  9625  fin1a2lem7  10351  prlem934  10978  addlid  11347  addcom  11350  addcomd  11366  negeu  11400  add20  11676  2halves  12390  bcnn  14222  bcpasc  14231  hashfun  14347  hashf1dmrn  14353  wrdeqs1cat  14620  sqreulem  15256  summolem3  15610  fsumneg  15683  geolim  15766  geolim2  15767  mertens  15782  prodmolem3  15827  fallrisefac  15919  bpoly3  15952  sincossq  16069  demoivre  16093  eirrlem  16097  oddpwp1fsum  16285  sadeq  16363  gcdid  16418  gcdmultipled  16426  phiprmpw  16659  pythagtriplem12  16709  expnprm  16785  fullresc  17751  grpinvid1  18816  grpnpcan  18853  grplactcnv  18864  ghmgrp  18885  conjghm  19053  odmodnn0  19336  gex1  19387  sylow3lem3  19425  efgredeu  19548  odadd2  19641  gsumval3  19698  pgpfac1lem3a  19869  ringnegl  20032  ringnegr  20033  ringmneg2  20035  rdivmuldivd  20138  imadrhmcl  20320  lmodfopne  20417  lmodvsneg  20423  lss0v  20534  lssvs0or  20630  lvecinv  20633  lspabs2  20640  zringunit  20924  zringcyg  20927  mplcoe3  21476  mplcoe5  21478  evlvar  21547  mdetrlin  21988  mdetunilem6  22003  cramerimplem3  22071  cramerimp  22072  paste  22682  tuslem  23655  tuslemOLD  23656  tususs  23659  ngpds  23997  ioo2bl  24193  ipcau2  24635  dvexp3  25379  rolle  25391  cmvth  25392  dv11cn  25402  lhop  25417  itgsubstlem  25449  itgpowd  25451  ply1divex  25538  fta1glem1  25567  fta1g  25569  dgrnznn  25645  fta1  25705  vieta1lem2  25708  aaliou2  25737  dvtaylp  25766  dvntaylp  25767  taylthlem1  25769  taylthlem2  25770  dvradcnv  25817  ptolemy  25890  coskpi  25916  tanregt0  25932  cxpeq  26147  isosctrlem2  26206  chordthmlem  26219  dcubic  26233  quart1lem  26242  tanatan  26306  atantan  26310  dvatan  26322  birthdaylem2  26339  rlimcxp  26360  jensenlem2  26374  logdiflbnd  26381  emcllem2  26383  lgamgulmlem2  26416  lgamcvg2  26441  basellem8  26474  bclbnd  26665  lgsqr  26736  lgseisenlem3  26762  lgseisenlem4  26763  lgsquadlem1  26765  lgsquadlem2  26766  rpvmasumlem  26872  dchrisumlem1  26874  dchrisum0flblem1  26893  dchrisum0flblem2  26894  dchrisum0re  26898  dchrisum0lem1  26901  mudivsum  26915  mulogsum  26917  vmalogdivsum2  26923  logsqvma2  26928  selberg2lem  26935  logdivbnd  26941  selbergr  26953  selberg3r  26954  pntrlog2bndlem4  26965  pntrlog2bndlem5  26966  pntpbnd2  26972  miduniq  27690  krippenlem  27695  colperpexlem2  27736  ttgcontlem1  27896  brbtwn2  27917  colinearalglem4  27921  axsegconlem9  27937  ax5seglem1  27940  axbtwnid  27951  axeuclidlem  27974  axcontlem2  27977  axcontlem4  27979  grpoinvid1  29533  vcz  29580  hosubsub4  30823  lnop0  30971  branmfn  31110  fressupp  31670  difico  31754  wrdsplex  31864  s3f1  31873  ccatf1  31875  mgcf1o  31933  omndmul2  31990  cycpmco2lem4  32048  tocyccntz  32063  cyc3genpm  32071  cycpmconjslem2  32074  dvdschrmulg  32136  kerunit  32185  qustrivr  32225  fermltlchr  32226  znfermltl  32227  linds2eq  32241  ply1degltdimlem  32404  fedgmullem2  32412  carsggect  33007  carsgclctunlem2  33008  ballotlemfrceq  33217  ballotlemrinv0  33221  hashreprin  33322  hgt750lemb  33358  faclimlem1  34402  irrdifflemf  35869  poimirlem4  36155  poimirlem23  36174  mblfinlem2  36189  voliunnfl  36195  volsupnfl  36196  itg2addnclem3  36204  ftc2nc  36233  dvasin  36235  areacirclem1  36239  areacirclem4  36242  rngonegmn1l  36473  rngonegmn1r  36474  lfl0  37600  latmassOLD  37764  omlmod1i2N  37795  llnexchb2lem  38404  dalawlem3  38409  pmapj2N  38465  osumcllem9N  38500  pexmidlem6N  38511  4atexlemc  38605  cdleme1  38763  cdleme42a  39007  cdlemg13a  39187  cdlemh2  39352  cdlemk1  39367  tendocnv  39557  dihmeetlem12N  39854  dihmeetlem16N  39858  dihmeetlem19N  39861  dochsatshp  39987  dochexmidlem6  40001  mapdval4N  40168  mapdpglem28  40237  mapdpglem31  40239  mapdindp4  40259  hdmap14lem1a  40402  hdmapinvlem4  40457  oexpreposd  40865  nn0rppwr  40877  sn-00idlem3  40927  remul01  40934  sn-subeu  40953  remulinvcom  40959  sn-0tie0  40966  cnreeu  40995  fltnlta  41059  irrapxlem5  41207  pellfund14  41279  rmxdbl  41321  jm2.22  41377  oaabsb  41687  oaun2  41774  oaun3  41775  sqrtcval  42035  0ellimcdiv  44010  fourierdlem95  44562  etransclem46  44641  sigariz  45224  ichreuopeq  45785  isomushgr  46138  altgsumbc  46548  blengt1fldiv2p1  46799  restclsseplem  47067