Theorem 3eqtr3rd 2809

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

Syntax hints:   → wi 4   = wceq 1563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757

This theorem is referenced by:  iunxdif3  5057  fcofo  7276  fcof1oinvd  7281  cantnfp1lem3  9637  fin1a2lem7  10378  prlem934  11006  addlid  11381  addcom  11384  addcomd  11400  negeu  11435  add20  11714  2halves  12453  bcnn  14339  bcpasc  14348  hashfun  14464  hashf1dmrn  14470  wrdeqs1cat  14747  sqreulem  15401  summolem3  15755  fsumneg  15828  geolim  15914  geolim2  15915  mertens  15930  prodmolem3  15977  fallrisefac  16069  bpoly3  16102  sincossq  16222  demoivre  16246  eirrlem  16250  oddpwp1fsum  16440  sadeq  16520  gcdid  16575  gcdmultipled  16582  nn0rppwr  16609  phiprmpw  16825  pythagtriplem12  16876  expnprm  16952  fullresc  17898  grpinvid1  19048  grpnpcan  19089  grplactcnv  19100  ghmgrp  19123  qustrivr  19244  conjghm  19310  odmodnn0  19601  gex1  19652  sylow3lem3  19690  efgredeu  19813  odadd2  19910  gsumval3  19968  pgpfac1lem3a  20139  omndmul2  20194  ringnegl  20376  ringnegr  20377  ringmneg2  20379  rdivmuldivd  20486  imadrhmcl  20869  lmodfopne  20990  lmodvsneg  20996  lssvs0or  21203  lvecinv  21206  lspabs2  21213  zringunit  21576  zringcyg  21579  dvdschrmulg  21638  fermltlchr  21639  sraassab  21978  mplcoe3  22149  mplcoe5  22151  evlvar  22219  psd1  22290  mdetrlin  22720  mdetunilem6  22735  cramerimplem3  22803  cramerimp  22804  paste  23412  tuslem  24384  tususs  24387  ngpds  24722  ioo2bl  24911  ipcau2  25354  dvexp3  26098  rolle  26110  cmvth  26111  dv11cn  26121  lhop  26136  itgsubstlem  26168  itgpowd  26170  ply1divex  26255  fta1glem1  26286  fta1g  26288  dgrnznn  26365  fta1  26430  vieta1lem2  26433  aaliou2  26462  dvtaylp  26491  dvntaylp  26492  taylthlem1  26494  taylthlem2  26495  dvradcnv  26542  ptolemy  26619  coskpi  26646  tanregt0  26662  cxpeq  26880  isosctrlem2  26942  chordthmlem  26955  dcubic  26969  quart1lem  26978  tanatan  27042  atantan  27046  dvatan  27058  birthdaylem2  27075  rlimcxp  27096  jensenlem2  27110  logdiflbnd  27117  emcllem2  27119  lgamgulmlem2  27152  lgamcvg2  27177  basellem8  27210  bclbnd  27402  lgsqr  27473  lgseisenlem3  27499  lgseisenlem4  27500  lgsquadlem1  27502  lgsquadlem2  27503  rpvmasumlem  27609  dchrisumlem1  27611  dchrisum0flblem1  27630  dchrisum0flblem2  27631  dchrisum0re  27635  dchrisum0lem1  27638  mudivsum  27652  mulogsum  27654  vmalogdivsum2  27660  logsqvma2  27665  selberg2lem  27672  logdivbnd  27678  selbergr  27690  selberg3r  27691  pntrlog2bndlem4  27702  pntrlog2bndlem5  27703  pntpbnd2  27709  pw2divscan4d  28595  pw2cutp1  28612  pw2cut2  28613  z12zsodd  28633  miduniq  28916  krippenlem  28921  colperpexlem2  28962  plngrotlem1  29017  ttgcontlem1  29143  brbtwn2  29164  colinearalglem4  29168  axsegconlem9  29184  ax5seglem1  29187  axbtwnid  29198  axeuclidlem  29221  axcontlem2  29224  axcontlem4  29226  grpoinvid1  30789  vcz  30836  hosubsub4  32079  lnop0  32227  branmfn  32366  fressupp  32945  difico  33040  wrdsplex  33169  s3f1  33180  ccatf1  33182  mgcf1o  33236  mndlrinv  33257  cycpmco2lem4  33362  tocyccntz  33377  cyc3genpm  33385  cycpmconjslem2  33388  rlocisunit  33509  kerunit  33560  znfermltl  33596  linds2eq  33610  dvdsruassoi  33613  dvdsruasso  33614  qsdrnglem2  33695  zringfrac  33761  m1pmeq  33792  vr1nz  33800  mplvrpmrhm  33854  esplyfval1  33880  ply1degltdimlem  33929  fedgmullem2  33937  fldextrspunlsplem  33980  constrrtll  34038  constrrtlc1  34039  constrrtcclem  34041  constrrtcc  34042  constrrecl  34076  2sqr3minply  34087  cos9thpiminplylem1  34089  cos9thpiminplylem2  34090  carsggect  34625  carsgclctunlem2  34626  ballotlemfrceq  34836  ballotlemrinv0  34840  hashreprin  34924  hgt750lemb  34960  faclimlem1  36106  irrdifflemf  37829  poimirlem4  38135  poimirlem23  38154  mblfinlem2  38169  voliunnfl  38175  volsupnfl  38176  itg2addnclem3  38184  ftc2nc  38213  dvasin  38215  areacirclem1  38219  areacirclem4  38222  rngonegmn1l  38452  rngonegmn1r  38453  lfl0  39701  latmassOLD  39865  omlmod1i2N  39896  llnexchb2lem  40504  dalawlem3  40509  pmapj2N  40565  osumcllem9N  40600  pexmidlem6N  40611  4atexlemc  40705  cdleme1  40863  cdleme42a  41107  cdlemg13a  41287  cdlemh2  41452  cdlemk1  41467  tendocnv  41657  dihmeetlem12N  41954  dihmeetlem16N  41958  dihmeetlem19N  41961  dochsatshp  42087  dochexmidlem6  42101  mapdval4N  42268  mapdpglem28  42337  mapdpglem31  42339  mapdindp4  42359  hdmap14lem1a  42502  hdmapinvlem4  42557  3rdpwhole  42913  oexpreposd  42943  remul01  43028  sn-negex12  43038  sn-subeu  43048  remulinvcom  43054  sn-0tie0  43085  cnreeu  43124  fltnlta  43257  irrapxlem5  43415  pellfund14  43487  rmxdbl  43528  jm2.22  43584  oaabsb  43883  oaun2  43970  oaun3  43971  sqrtcval  44229  0ellimcdiv  46221  fourierdlem95  46773  etransclem46  46852  sigariz  47435  sin5tlem2  47466  sin5tlem5  47469  cos5t  47471  ichreuopeq  48077  gricushgr  48537  altgsumbc  48983  blengt1fldiv2p1  49224  restclsseplem  49544  cofu1a  49723  cofu2a  49724  uobeqw  49848  swapf2fval  49894  swapf1val  49896  coccom  50293