Theorem 3eqtr3rd 2823

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

Syntax hints:   → wi 4   = wceq 1601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770

This theorem is referenced by:  iunxdif3  4842  fcofo  6817  fcof1oinvd  6822  cantnfp1lem3  8876  fin1a2lem7  9565  prlem934  10192  addid2  10561  addcom  10564  addcomd  10580  negeu  10614  add20  10889  2halves  11614  bcnn  13421  bcpasc  13430  hashfun  13542  wrdeqs1cat  13843  wrdeqs1catOLD  13844  sqreulem  14510  summolem3  14856  fsumneg  14927  geolim  15009  geolim2  15010  mertens  15025  prodmolem3  15070  fallrisefac  15162  bpoly3  15195  sincossq  15312  demoivre  15336  eirrlem  15340  oddpwp1fsum  15526  sadeq  15604  gcdid  15658  phiprmpw  15889  pythagtriplem12  15939  expnprm  16014  fullresc  16900  grpinvid1  17861  grpnpcan  17898  grplactcnv  17909  ghmgrp  17930  conjghm  18079  odmodnn0  18347  gex1  18394  sylow3lem3  18432  efgredeu  18555  odadd2  18642  gsumval3  18698  pgpfac1lem3a  18866  ringnegl  18985  rngnegr  18986  ringmneg2  18988  lmodfopne  19297  lmodvsneg  19303  lss0v  19415  lssvs0or  19509  lvecinv  19512  lspabs2  19519  mplcoe3  19867  mplcoe5  19869  evlvar  19929  zringunit  20236  zringcyg  20239  mdetrlin  20817  mdetunilem6  20832  cramerimplem3  20902  cramerimp  20903  paste  21510  tuslem  22483  tususs  22486  ngpds  22820  ioo2bl  23008  ipcau2  23444  dvexp3  24182  rolle  24194  cmvth  24195  dv11cn  24205  lhop  24220  itgsubstlem  24252  ply1divex  24337  fta1glem1  24366  fta1g  24368  dgrnznn  24444  fta1  24504  vieta1lem2  24507  aaliou2  24536  dvtaylp  24565  dvntaylp  24566  taylthlem1  24568  taylthlem2  24569  dvradcnv  24616  ptolemy  24690  coskpi  24714  tanregt0  24727  cxpeq  24942  isosctrlem2  25001  chordthmlem  25014  dcubic  25028  quart1lem  25037  tanatan  25101  atantan  25105  dvatan  25117  birthdaylem2  25135  rlimcxp  25156  jensenlem2  25170  logdiflbnd  25177  emcllem2  25179  lgamgulmlem2  25212  lgamcvg2  25237  basellem8  25270  bclbnd  25461  lgsqr  25532  lgseisenlem3  25558  lgseisenlem4  25559  lgsquadlem1  25561  lgsquadlem2  25562  rpvmasumlem  25632  dchrisumlem1  25634  dchrisum0flblem1  25653  dchrisum0flblem2  25654  dchrisum0re  25658  dchrisum0lem1  25661  mudivsum  25675  mulogsum  25677  vmalogdivsum2  25683  logsqvma2  25688  selberg2lem  25695  logdivbnd  25701  selbergr  25713  selberg3r  25714  pntrlog2bndlem4  25725  pntrlog2bndlem5  25726  pntpbnd2  25732  miduniq  26040  krippenlem  26045  colperpexlem2  26083  ttgcontlem1  26238  brbtwn2  26258  colinearalglem4  26262  axsegconlem9  26278  ax5seglem1  26281  axbtwnid  26292  axeuclidlem  26315  axcontlem2  26318  axcontlem4  26320  clwwlkel  27441  grpoinvid1  27959  vcz  28006  hosubsub4  29253  lnop0  29401  branmfn  29540  difico  30113  omndmul2  30278  rdivmuldivd  30357  kerunit  30389  carsggect  30982  carsgclctunlem2  30983  ballotlemfrceq  31193  ballotlemrinv0  31197  wrdsplex  31221  wrdsplexOLD  31222  hashreprin  31304  hgt750lemb  31340  faclimlem1  32227  poimirlem4  34044  poimirlem23  34063  mblfinlem2  34078  voliunnfl  34084  volsupnfl  34085  itg2addnclem3  34093  ftc2nc  34124  dvasin  34126  areacirclem1  34130  areacirclem4  34133  rngonegmn1l  34369  rngonegmn1r  34370  lfl0  35224  latmassOLD  35388  omlmod1i2N  35419  llnexchb2lem  36027  dalawlem3  36032  pmapj2N  36088  osumcllem9N  36123  pexmidlem6N  36134  4atexlemc  36228  cdleme1  36386  cdleme42a  36630  cdlemg13a  36810  cdlemh2  36975  cdlemk1  36990  tendocnv  37180  dihmeetlem12N  37477  dihmeetlem16N  37481  dihmeetlem19N  37484  dochsatshp  37610  dochexmidlem6  37624  mapdval4N  37791  mapdpglem28  37860  mapdpglem31  37862  mapdindp4  37882  hdmap14lem1a  38025  hdmapinvlem4  38080  oexpreposd  38165  nn0rppwr  38168  irrapxlem5  38360  pellfund14  38432  rmxdbl  38473  jm2.22  38531  itgpowd  38768  0ellimcdiv  40799  fourierdlem95  41355  etransclem46  41434  sigariz  41989  isomushgr  42749  altgsumbc  43155  blengt1fldiv2p1  43412