Theorem 3eqtr3rd 2786

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  iunxdif3  5095  fcofo  7308  fcof1oinvd  7313  cantnfp1lem3  9720  fin1a2lem7  10446  prlem934  11073  addlid  11444  addcom  11447  addcomd  11463  negeu  11498  add20  11775  2halves  12494  bcnn  14351  bcpasc  14360  hashfun  14476  hashf1dmrn  14482  wrdeqs1cat  14758  sqreulem  15398  summolem3  15750  fsumneg  15823  geolim  15906  geolim2  15907  mertens  15922  prodmolem3  15969  fallrisefac  16061  bpoly3  16094  sincossq  16212  demoivre  16236  eirrlem  16240  oddpwp1fsum  16429  sadeq  16509  gcdid  16564  gcdmultipled  16571  nn0rppwr  16598  phiprmpw  16813  pythagtriplem12  16864  expnprm  16940  fullresc  17896  grpinvid1  19009  grpnpcan  19050  grplactcnv  19061  ghmgrp  19084  conjghm  19267  odmodnn0  19558  gex1  19609  sylow3lem3  19647  efgredeu  19770  odadd2  19867  gsumval3  19925  pgpfac1lem3a  20096  ringnegl  20299  ringnegr  20300  ringmneg2  20302  rdivmuldivd  20413  imadrhmcl  20798  lmodfopne  20898  lmodvsneg  20904  lssvs0or  21112  lvecinv  21115  lspabs2  21122  zringunit  21477  zringcyg  21480  dvdschrmulg  21543  fermltlchr  21544  sraassab  21888  mplcoe3  22056  mplcoe5  22058  evlvar  22124  psd1  22171  mdetrlin  22608  mdetunilem6  22623  cramerimplem3  22691  cramerimp  22692  paste  23302  tuslem  24275  tuslemOLD  24276  tususs  24279  ngpds  24617  ioo2bl  24814  ipcau2  25268  dvexp3  26016  rolle  26028  cmvth  26029  cmvthOLD  26030  dv11cn  26040  lhop  26055  itgsubstlem  26089  itgpowd  26091  ply1divex  26176  fta1glem1  26207  fta1g  26209  dgrnznn  26286  fta1  26350  vieta1lem2  26353  aaliou2  26382  dvtaylp  26412  dvntaylp  26413  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  dvradcnv  26464  ptolemy  26538  coskpi  26565  tanregt0  26581  cxpeq  26800  isosctrlem2  26862  chordthmlem  26875  dcubic  26889  quart1lem  26898  tanatan  26962  atantan  26966  dvatan  26978  birthdaylem2  26995  rlimcxp  27017  jensenlem2  27031  logdiflbnd  27038  emcllem2  27040  lgamgulmlem2  27073  lgamcvg2  27098  basellem8  27131  bclbnd  27324  lgsqr  27395  lgseisenlem3  27421  lgseisenlem4  27422  lgsquadlem1  27424  lgsquadlem2  27425  rpvmasumlem  27531  dchrisumlem1  27533  dchrisum0flblem1  27552  dchrisum0flblem2  27553  dchrisum0re  27557  dchrisum0lem1  27560  mudivsum  27574  mulogsum  27576  vmalogdivsum2  27582  logsqvma2  27587  selberg2lem  27594  logdivbnd  27600  selbergr  27612  selberg3r  27613  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntpbnd2  27631  miduniq  28693  krippenlem  28698  colperpexlem2  28739  ttgcontlem1  28899  brbtwn2  28920  colinearalglem4  28924  axsegconlem9  28940  ax5seglem1  28943  axbtwnid  28954  axeuclidlem  28977  axcontlem2  28980  axcontlem4  28982  grpoinvid1  30547  vcz  30594  hosubsub4  31837  lnop0  31985  branmfn  32124  fressupp  32697  difico  32785  wrdsplex  32920  s3f1  32931  ccatf1  32933  mgcf1o  32993  mndlrinv  33029  omndmul2  33089  cycpmco2lem4  33149  tocyccntz  33164  cyc3genpm  33172  cycpmconjslem2  33175  kerunit  33349  qustrivr  33393  znfermltl  33394  linds2eq  33409  dvdsruassoi  33412  dvdsruasso  33413  qsdrnglem2  33524  zringfrac  33582  m1pmeq  33608  ply1degltdimlem  33673  fedgmullem2  33681  fldextrspunlsplem  33723  constrrtll  33772  constrrtlc1  33773  constrrtcclem  33775  constrrtcc  33776  2sqr3minply  33791  carsggect  34320  carsgclctunlem2  34321  ballotlemfrceq  34531  ballotlemrinv0  34535  hashreprin  34635  hgt750lemb  34671  faclimlem1  35743  irrdifflemf  37326  poimirlem4  37631  poimirlem23  37650  mblfinlem2  37665  voliunnfl  37671  volsupnfl  37672  itg2addnclem3  37680  ftc2nc  37709  dvasin  37711  areacirclem1  37715  areacirclem4  37718  rngonegmn1l  37948  rngonegmn1r  37949  lfl0  39066  latmassOLD  39230  omlmod1i2N  39261  llnexchb2lem  39870  dalawlem3  39875  pmapj2N  39931  osumcllem9N  39966  pexmidlem6N  39977  4atexlemc  40071  cdleme1  40229  cdleme42a  40473  cdlemg13a  40653  cdlemh2  40818  cdlemk1  40833  tendocnv  41023  dihmeetlem12N  41320  dihmeetlem16N  41324  dihmeetlem19N  41327  dochsatshp  41453  dochexmidlem6  41467  mapdval4N  41634  mapdpglem28  41703  mapdpglem31  41705  mapdindp4  41725  hdmap14lem1a  41868  hdmapinvlem4  41923  oexpreposd  42357  sn-00idlem3  42430  remul01  42437  sn-negex12  42446  sn-subeu  42456  remulinvcom  42462  sn-0tie0  42469  cnreeu  42500  fltnlta  42673  irrapxlem5  42837  pellfund14  42909  rmxdbl  42951  jm2.22  43007  oaabsb  43307  oaun2  43394  oaun3  43395  sqrtcval  43654  0ellimcdiv  45664  fourierdlem95  46216  etransclem46  46295  sigariz  46878  ichreuopeq  47460  gricushgr  47886  altgsumbc  48268  blengt1fldiv2p1  48514  restclsseplem  48812  swapf2fval  48971  swapf1val  48973