Theorem 3eqtr3rd 2805

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

Syntax hints:   → wi 4   = wceq 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  iunxdif3  5051  fcofo  7268  fcof1oinvd  7273  cantnfp1lem3  9632  fin1a2lem7  10360  prlem934  10988  addlid  11363  addcom  11366  addcomd  11382  negeu  11417  add20  11696  2halves  12436  bcnn  14322  bcpasc  14331  hashfun  14447  hashf1dmrn  14453  wrdeqs1cat  14730  sqreulem  15370  summolem3  15724  fsumneg  15797  geolim  15883  geolim2  15884  mertens  15899  prodmolem3  15946  fallrisefac  16038  bpoly3  16071  sincossq  16191  demoivre  16215  eirrlem  16219  oddpwp1fsum  16409  sadeq  16489  gcdid  16544  gcdmultipled  16551  nn0rppwr  16578  phiprmpw  16794  pythagtriplem12  16845  expnprm  16921  fullresc  17867  grpinvid1  19016  grpnpcan  19057  grplactcnv  19068  ghmgrp  19091  conjghm  19272  odmodnn0  19563  gex1  19614  sylow3lem3  19652  efgredeu  19775  odadd2  19872  gsumval3  19930  pgpfac1lem3a  20101  omndmul2  20156  ringnegl  20331  ringnegr  20332  ringmneg2  20334  rdivmuldivd  20441  imadrhmcl  20826  lmodfopne  20947  lmodvsneg  20953  lssvs0or  21160  lvecinv  21163  lspabs2  21170  zringunit  21498  zringcyg  21501  dvdschrmulg  21560  fermltlchr  21561  sraassab  21900  mplcoe3  22071  mplcoe5  22073  evlvar  22141  psd1  22212  mdetrlin  22642  mdetunilem6  22657  cramerimplem3  22725  cramerimp  22726  paste  23334  tuslem  24306  tususs  24309  ngpds  24644  ioo2bl  24833  ipcau2  25276  dvexp3  26020  rolle  26032  cmvth  26033  dv11cn  26043  lhop  26058  itgsubstlem  26090  itgpowd  26092  ply1divex  26177  fta1glem1  26208  fta1g  26210  dgrnznn  26287  fta1  26349  vieta1lem2  26352  aaliou2  26381  dvtaylp  26410  dvntaylp  26411  taylthlem1  26413  taylthlem2  26414  dvradcnv  26461  ptolemy  26538  coskpi  26565  tanregt0  26581  cxpeq  26799  isosctrlem2  26861  chordthmlem  26874  dcubic  26888  quart1lem  26897  tanatan  26961  atantan  26965  dvatan  26977  birthdaylem2  26994  rlimcxp  27015  jensenlem2  27029  logdiflbnd  27036  emcllem2  27038  lgamgulmlem2  27071  lgamcvg2  27096  basellem8  27129  bclbnd  27321  lgsqr  27392  lgseisenlem3  27418  lgseisenlem4  27419  lgsquadlem1  27421  lgsquadlem2  27422  rpvmasumlem  27528  dchrisumlem1  27530  dchrisum0flblem1  27549  dchrisum0flblem2  27550  dchrisum0re  27554  dchrisum0lem1  27557  mudivsum  27571  mulogsum  27573  vmalogdivsum2  27579  logsqvma2  27584  selberg2lem  27591  logdivbnd  27597  selbergr  27609  selberg3r  27610  pntrlog2bndlem4  27621  pntrlog2bndlem5  27622  pntpbnd2  27628  pw2divscan4d  28514  pw2cutp1  28531  pw2cut2  28532  z12zsodd  28552  miduniq  28831  krippenlem  28836  colperpexlem2  28877  ttgcontlem1  29031  brbtwn2  29052  colinearalglem4  29056  axsegconlem9  29072  ax5seglem1  29075  axbtwnid  29086  axeuclidlem  29109  axcontlem2  29112  axcontlem4  29114  grpoinvid1  30677  vcz  30724  hosubsub4  31967  lnop0  32115  branmfn  32254  fressupp  32840  difico  32935  wrdsplex  33075  s3f1  33086  ccatf1  33088  mgcf1o  33142  mndlrinv  33163  cycpmco2lem4  33270  tocyccntz  33285  cyc3genpm  33293  cycpmconjslem2  33296  rlocisunit  33418  kerunit  33472  qustrivr  33512  znfermltl  33513  linds2eq  33528  dvdsruassoi  33531  dvdsruasso  33532  qsdrnglem2  33645  zringfrac  33711  m1pmeq  33742  vr1nz  33750  mplvrpmrhm  33805  esplyfval1  33831  ply1degltdimlem  33880  fedgmullem2  33888  fldextrspunlsplem  33931  constrrtll  33989  constrrtlc1  33990  constrrtcclem  33992  constrrtcc  33993  constrrecl  34027  2sqr3minply  34038  cos9thpiminplylem1  34040  cos9thpiminplylem2  34041  carsggect  34576  carsgclctunlem2  34577  ballotlemfrceq  34787  ballotlemrinv0  34791  hashreprin  34878  hgt750lemb  34914  faclimlem1  36057  irrdifflemf  37781  poimirlem4  38087  poimirlem23  38106  mblfinlem2  38121  voliunnfl  38127  volsupnfl  38128  itg2addnclem3  38136  ftc2nc  38165  dvasin  38167  areacirclem1  38171  areacirclem4  38174  rngonegmn1l  38404  rngonegmn1r  38405  lfl0  39653  latmassOLD  39817  omlmod1i2N  39848  llnexchb2lem  40456  dalawlem3  40461  pmapj2N  40517  osumcllem9N  40552  pexmidlem6N  40563  4atexlemc  40657  cdleme1  40815  cdleme42a  41059  cdlemg13a  41239  cdlemh2  41404  cdlemk1  41419  tendocnv  41609  dihmeetlem12N  41906  dihmeetlem16N  41910  dihmeetlem19N  41913  dochsatshp  42039  dochexmidlem6  42053  mapdval4N  42220  mapdpglem28  42289  mapdpglem31  42291  mapdindp4  42311  hdmap14lem1a  42454  hdmapinvlem4  42509  3rdpwhole  42865  oexpreposd  42895  remul01  42980  sn-negex12  42990  sn-subeu  43000  remulinvcom  43006  sn-0tie0  43037  cnreeu  43076  fltnlta  43209  irrapxlem5  43367  pellfund14  43439  rmxdbl  43480  jm2.22  43536  oaabsb  43835  oaun2  43922  oaun3  43923  sqrtcval  44181  0ellimcdiv  46187  fourierdlem95  46739  etransclem46  46818  sigariz  47401  sin5tlem2  47432  sin5tlem5  47435  cos5t  47437  ichreuopeq  48043  gricushgr  48503  altgsumbc  48938  blengt1fldiv2p1  49179  restclsseplem  49500  cofu1a  49679  cofu2a  49680  uobeqw  49804  swapf2fval  49850  swapf1val  49852  coccom  50249