Theorem 3eqtr3rd 2806

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754

This theorem is used by:  iunxdif3  5059  fcofo  7293  fcof1oinvd  7298  cantnfp1lem3  9663  fin1a2lem7  10412  prlem934  11046  addlid  11421  addcom  11424  addcomd  11440  negeu  11475  add20  11754  2halves  12490  bcnn  14380  bcpasc  14389  hashfun  14506  hashf1dmrn  14512  ccatf1  14660  wrdeqs1cat  14793  sqreulem  15451  summolem3  15804  fsumneg  15877  geolim  15963  geolim2  15964  mertens  15979  prodmolem3  16026  fallrisefac  16118  bpoly3  16150  sincossq  16270  demoivre  16294  eirrlem  16298  oddpwp1fsum  16488  sadeq  16568  gcdid  16623  gcdmultipled  16630  nn0rppwr  16657  phiprmpw  16873  pythagtriplem12  16924  expnprm  17000  fullresc  17946  grpinvid1  19121  grpnpcan  19161  grplactcnv  19172  ghmgrp  19195  qustrivr  19316  conjghm  19382  odmodnn0  19673  gex1  19724  sylow3lem3  19762  efgredeu  19885  odadd2  19982  gsumval3  20040  pgpfac1lem3a  20211  omndmul2  20266  ringnegl  20450  ringnegr  20451  ringmneg2  20453  rdivmuldivd  20560  imadrhmcl  20969  lmodfopne  21090  lmodvsneg  21096  lssvs0or  21303  lvecinv  21306  lspabs2  21313  zringunit  21685  zringcyg  21688  dvdschrmulg  21747  fermltlchr  21748  sraassab  22089  mplcoe3  22260  mplcoe5  22262  evlvar  22330  psd1  22401  mdetrlin  22830  mdetunilem6  22845  cramerimplem3  22916  cramerimp  22917  paste  23525  tuslem  24498  tususs  24501  ngpds  24836  ioo2bl  25025  ipcau2  25468  dvexp3  26212  rolle  26224  cmvth  26225  dv11cn  26235  lhop  26250  itgsubstlem  26282  itgpowd  26284  ply1divex  26369  fta1glem1  26400  fta1g  26402  dgrnznn  26480  fta1  26545  vieta1lem2  26550  aaliou2  26583  dvtaylp  26613  dvntaylp  26614  taylthlem1  26616  taylthlem2  26617  dvradcnv  26664  ptolemy  26741  coskpi  26768  tanregt0  26784  cxpeq  27002  isosctrlem2  27064  chordthmlem  27077  dcubic  27091  quart1lem  27100  tanatan  27164  atantan  27168  dvatan  27180  birthdaylem2  27197  rlimcxp  27218  jensenlem2  27232  logdiflbnd  27239  emcllem2  27241  lgamgulmlem2  27274  lgamcvg2  27299  basellem8  27332  bclbnd  27524  lgsqr  27595  lgseisenlem3  27621  lgseisenlem4  27622  lgsquadlem1  27624  lgsquadlem2  27625  rpvmasumlem  27731  dchrisumlem1  27733  dchrisum0flblem1  27752  dchrisum0flblem2  27753  dchrisum0re  27757  dchrisum0lem1  27760  mudivsum  27774  mulogsum  27776  vmalogdivsum2  27782  logsqvma2  27787  selberg2lem  27794  logdivbnd  27800  selbergr  27812  selberg3r  27813  pntrlog2bndlem4  27824  pntrlog2bndlem5  27825  pntpbnd2  27831  pw2divscan4d  28717  pw2cutp1  28734  pw2cut2  28735  z12zsodd  28755  miduniq  29044  krippenlem  29049  colperpexlem2  29094  plngrotlem1  29152  ttgcontlem1  29349  brbtwn2  29370  colinearalglem4  29374  axsegconlem9  29390  ax5seglem1  29393  axbtwnid  29404  axeuclidlem  29427  axcontlem2  29430  axcontlem4  29432  grpoinvid1  31017  vcz  31064  hosubsub4  32307  lnop0  32455  branmfn  32594  fressupp  33168  difico  33262  wrdsplex  33390  s3f1  33398  mgcf1o  33451  mndlrinv  33472  cycpmco2lem4  33577  tocyccntz  33592  cyc3genpm  33600  cycpmconjslem2  33603  rlocisunit  33724  kerunit  33773  znfermltl  33809  linds2eq  33822  dvdsruassoi  33825  dvdsruasso  33826  qsdrnglem2  33906  zringfrac  33972  m1pmeq  34003  vr1nz  34011  mplvrpmrhm  34065  esplyfval1  34091  ply1degltdimlem  34140  fedgmullem2  34148  fldextrspunlsplem  34191  constrrtll  34249  constrrtlc1  34250  constrrtcclem  34252  constrrtcc  34253  constrrecl  34287  2sqr3minply  34298  cos9thpiminplylem1  34300  cos9thpiminplylem2  34301  carsggect  34837  carsgclctunlem2  34838  ballotlemfrceq  35048  ballotlemrinv0  35052  hashreprin  35136  hgt750lemb  35172  faclimlem1  36330  irrdifflemf  38085  poimirlem4  38381  poimirlem23  38400  mblfinlem2  38415  voliunnfl  38421  volsupnfl  38422  itg2addnclem3  38430  ftc2nc  38459  dvasin  38461  areacirclem1  38465  areacirclem4  38468  rngonegmn1l  38699  rngonegmn1r  38700  lfl0  39946  latmassOLD  40110  omlmod1i2N  40141  llnexchb2lem  40749  dalawlem3  40754  pmapj2N  40810  osumcllem9N  40845  pexmidlem6N  40856  4atexlemc  40950  cdleme1  41108  cdleme42a  41352  cdlemg13a  41532  cdlemh2  41697  cdlemk1  41712  tendocnv  41902  dihmeetlem12N  42199  dihmeetlem16N  42203  dihmeetlem19N  42206  dochsatshp  42332  dochexmidlem6  42346  mapdval4N  42513  mapdpglem28  42582  mapdpglem31  42584  mapdindp4  42604  hdmap14lem1a  42747  hdmapinvlem4  42802  3rdpwhole  43175  oexpreposd  43205  remul01  43290  sn-negex12  43300  sn-subeu  43310  remulinvcom  43316  sn-0tie0  43347  cnreeu  43386  fltnlta  43517  irrapxlem5  43675  pellfund14  43747  rmxdbl  43788  jm2.22  43844  oaabsb  44143  oaun2  44230  oaun3  44231  sqrtcval  44489  0ellimcdiv  46485  fourierdlem95  47037  etransclem46  47116  sigariz  47699  sin5tlem2  47746  sin5tlem5  47749  cos5t  47751  ichreuopeq  48381  gricushgr  48841  altgsumbc  49290  blengt1fldiv2p1  49531  restclsseplem  49849  cofu1a  50028  cofu2a  50029  uobeqw  50153  swapf2fval  50199  swapf1val  50201  coccom  50598