Theorem 3eqtr3rd 2781

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

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

This theorem is referenced by:  iunxdif3  5052  fcofo  7244  fcof1oinvd  7249  cantnfp1lem3  9601  fin1a2lem7  10328  prlem934  10956  addlid  11328  addcom  11331  addcomd  11347  negeu  11382  add20  11661  2halves  12371  bcnn  14247  bcpasc  14256  hashfun  14372  hashf1dmrn  14378  wrdeqs1cat  14655  sqreulem  15295  summolem3  15649  fsumneg  15722  geolim  15805  geolim2  15806  mertens  15821  prodmolem3  15868  fallrisefac  15960  bpoly3  15993  sincossq  16113  demoivre  16137  eirrlem  16141  oddpwp1fsum  16331  sadeq  16411  gcdid  16466  gcdmultipled  16473  nn0rppwr  16500  phiprmpw  16715  pythagtriplem12  16766  expnprm  16842  fullresc  17787  grpinvid1  18933  grpnpcan  18974  grplactcnv  18985  ghmgrp  19008  conjghm  19190  odmodnn0  19481  gex1  19532  sylow3lem3  19570  efgredeu  19693  odadd2  19790  gsumval3  19848  pgpfac1lem3a  20019  omndmul2  20074  ringnegl  20249  ringnegr  20250  ringmneg2  20252  rdivmuldivd  20361  imadrhmcl  20742  lmodfopne  20863  lmodvsneg  20869  lssvs0or  21077  lvecinv  21080  lspabs2  21087  zringunit  21433  zringcyg  21436  dvdschrmulg  21495  fermltlchr  21496  sraassab  21835  mplcoe3  22005  mplcoe5  22007  evlvar  22075  psd1  22122  mdetrlin  22558  mdetunilem6  22573  cramerimplem3  22641  cramerimp  22642  paste  23250  tuslem  24222  tususs  24225  ngpds  24560  ioo2bl  24749  ipcau2  25202  dvexp3  25950  rolle  25962  cmvth  25963  cmvthOLD  25964  dv11cn  25974  lhop  25989  itgsubstlem  26023  itgpowd  26025  ply1divex  26110  fta1glem1  26141  fta1g  26143  dgrnznn  26220  fta1  26284  vieta1lem2  26287  aaliou2  26316  dvtaylp  26346  dvntaylp  26347  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  dvradcnv  26398  ptolemy  26473  coskpi  26500  tanregt0  26516  cxpeq  26735  isosctrlem2  26797  chordthmlem  26810  dcubic  26824  quart1lem  26833  tanatan  26897  atantan  26901  dvatan  26913  birthdaylem2  26930  rlimcxp  26952  jensenlem2  26966  logdiflbnd  26973  emcllem2  26975  lgamgulmlem2  27008  lgamcvg2  27033  basellem8  27066  bclbnd  27259  lgsqr  27330  lgseisenlem3  27356  lgseisenlem4  27357  lgsquadlem1  27359  lgsquadlem2  27360  rpvmasumlem  27466  dchrisumlem1  27468  dchrisum0flblem1  27487  dchrisum0flblem2  27488  dchrisum0re  27492  dchrisum0lem1  27495  mudivsum  27509  mulogsum  27511  vmalogdivsum2  27517  logsqvma2  27522  selberg2lem  27529  logdivbnd  27535  selbergr  27547  selberg3r  27548  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntpbnd2  27566  pw2divscan4d  28452  pw2cutp1  28469  pw2cut2  28470  z12zsodd  28490  miduniq  28769  krippenlem  28774  colperpexlem2  28815  ttgcontlem1  28969  brbtwn2  28990  colinearalglem4  28994  axsegconlem9  29010  ax5seglem1  29013  axbtwnid  29024  axeuclidlem  29047  axcontlem2  29050  axcontlem4  29052  grpoinvid1  30615  vcz  30662  hosubsub4  31905  lnop0  32053  branmfn  32192  fressupp  32777  difico  32873  wrdsplex  33028  s3f1  33039  ccatf1  33041  mgcf1o  33095  mndlrinv  33116  cycpmco2lem4  33222  tocyccntz  33237  cyc3genpm  33245  cycpmconjslem2  33248  kerunit  33417  qustrivr  33457  znfermltl  33458  linds2eq  33473  dvdsruassoi  33476  dvdsruasso  33477  qsdrnglem2  33588  zringfrac  33646  m1pmeq  33677  vr1nz  33685  mplvrpmrhm  33723  esplyfval1  33749  ply1degltdimlem  33799  fedgmullem2  33807  fldextrspunlsplem  33850  constrrtll  33908  constrrtlc1  33909  constrrtcclem  33911  constrrtcc  33912  constrrecl  33946  2sqr3minply  33957  cos9thpiminplylem1  33959  cos9thpiminplylem2  33960  carsggect  34495  carsgclctunlem2  34496  ballotlemfrceq  34706  ballotlemrinv0  34710  hashreprin  34797  hgt750lemb  34833  faclimlem1  35956  irrdifflemf  37577  poimirlem4  37872  poimirlem23  37891  mblfinlem2  37906  voliunnfl  37912  volsupnfl  37913  itg2addnclem3  37921  ftc2nc  37950  dvasin  37952  areacirclem1  37956  areacirclem4  37959  rngonegmn1l  38189  rngonegmn1r  38190  lfl0  39438  latmassOLD  39602  omlmod1i2N  39633  llnexchb2lem  40241  dalawlem3  40246  pmapj2N  40302  osumcllem9N  40337  pexmidlem6N  40348  4atexlemc  40442  cdleme1  40600  cdleme42a  40844  cdlemg13a  41024  cdlemh2  41189  cdlemk1  41204  tendocnv  41394  dihmeetlem12N  41691  dihmeetlem16N  41695  dihmeetlem19N  41698  dochsatshp  41824  dochexmidlem6  41838  mapdval4N  42005  mapdpglem28  42074  mapdpglem31  42076  mapdindp4  42096  hdmap14lem1a  42239  hdmapinvlem4  42294  3rdpwhole  42659  oexpreposd  42689  remul01  42774  sn-negex12  42784  sn-subeu  42794  remulinvcom  42800  sn-0tie0  42818  cnreeu  42857  fltnlta  43018  irrapxlem5  43180  pellfund14  43252  rmxdbl  43293  jm2.22  43349  oaabsb  43648  oaun2  43735  oaun3  43736  sqrtcval  43994  0ellimcdiv  46004  fourierdlem95  46556  etransclem46  46635  sigariz  47218  ichreuopeq  47830  gricushgr  48274  altgsumbc  48709  blengt1fldiv2p1  48950  restclsseplem  49271  cofu1a  49450  cofu2a  49451  uobeqw  49575  swapf2fval  49621  swapf1val  49623  coccom  50020