Theorem 3eqtr3rd 2804

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  iunxdif3  5054  fcofo  7296  fcof1oinvd  7301  cantnfp1lem3  9684  fin1a2lem7  10487  prlem934  11121  addlid  11496  addcom  11499  addcomd  11515  negeu  11550  add20  11831  2halves  12567  bcnn  14459  bcpasc  14468  hashfun  14585  hashf1dmrn  14591  ccatf1  14739  wrdeqs1cat  14873  sqreulem  15532  summolem3  15885  fsumneg  15958  geolim  16044  geolim2  16045  mertens  16060  prodmolem3  16105  fallrisefac  16197  bpoly3  16229  sincossq  16349  demoivre  16373  eirrlem  16377  oddpwp1fsum  16567  sadeq  16647  gcdid  16704  gcdmultipled  16712  nn0rppwr  16740  phiprmpw  16958  pythagtriplem12  17009  expnprm  17085  fullresc  18031  grpinvid1  19207  grpnpcan  19247  grplactcnv  19258  ghmgrp  19281  qustrivr  19402  conjghm  19468  odmodnn0  19759  gex1  19810  sylow3lem3  19848  efgredeu  19971  odadd2  20068  gsumval3  20126  pgpfac1lem3a  20297  omndmul2  20352  ringnegl  20538  ringnegr  20539  ringmneg2  20541  rdivmuldivd  20648  imadrhmcl  21059  lmodfopne  21180  lmodvsneg  21186  lssvs0or  21393  lvecinv  21396  lspabs2  21403  zringunit  21777  zringcyg  21780  dvdschrmulg  21839  fermltlchr  21840  sraassab  22181  mplcoe3  22352  mplcoe5  22354  evlvar  22422  psd1  22493  mdetrlin  22922  mdetunilem6  22937  cramerimplem3  23008  cramerimp  23009  paste  23617  tuslem  24590  tususs  24593  ngpds  24928  ioo2bl  25117  ipcau2  25560  dvexp3  26303  rolle  26315  cmvth  26316  dv11cn  26326  lhop  26341  itgsubstlem  26373  itgpowd  26375  ply1divex  26460  fta1glem1  26491  fta1g  26493  dgrnznn  26571  fta1  26634  vieta1lem2  26639  aaliou2  26672  dvtaylp  26702  dvntaylp  26703  taylthlem1  26705  taylthlem2  26706  dvradcnv  26753  ptolemy  26830  coskpi  26856  tanregt0  26872  cxpeq  27090  isosctrlem2  27152  chordthmlem  27165  dcubic  27179  quart1lem  27188  tanatan  27252  atantan  27256  dvatan  27268  birthdaylem2  27285  rlimcxp  27306  jensenlem2  27320  logdiflbnd  27327  emcllem2  27329  lgamgulmlem2  27362  lgamcvg2  27387  basellem8  27420  bclbnd  27612  lgsqr  27683  lgseisenlem3  27709  lgseisenlem4  27710  lgsquadlem1  27712  lgsquadlem2  27713  rpvmasumlem  27819  dchrisumlem1  27821  dchrisum0flblem1  27840  dchrisum0flblem2  27841  dchrisum0re  27845  dchrisum0lem1  27848  mudivsum  27862  mulogsum  27864  vmalogdivsum2  27870  logsqvma2  27875  selberg2lem  27882  logdivbnd  27888  selbergr  27900  selberg3r  27901  pntrlog2bndlem4  27912  pntrlog2bndlem5  27913  pntpbnd2  27919  pw2divscan4d  28835  pw2cutp1  28852  pw2cut2  28853  z12zsodd  28873  miduniq  29162  krippenlem  29167  colperpexlem2  29212  plngrotlem1  29270  ttgcontlem1  29467  brbtwn2  29488  colinearalglem4  29492  axsegconlem9  29508  ax5seglem1  29511  axbtwnid  29522  axeuclidlem  29545  axcontlem2  29548  axcontlem4  29550  grpoinvid1  31135  vcz  31182  hosubsub4  32425  lnop0  32573  branmfn  32712  fressupp  33328  difico  33421  wrdsplex  33549  s3f1  33557  mgcf1o  33610  mndlrinv  33631  cycpmco2lem4  33736  tocyccntz  33751  cyc3genpm  33759  cycpmconjslem2  33762  rlocisunit  33883  kerunit  33932  znfermltl  33968  linds2eq  33982  dvdsruassoi  33985  dvdsruasso  33986  qsdrnglem2  34066  zringfrac  34132  m1pmeq  34163  vr1nz  34171  mplvrpmrhm  34225  esplyfval1  34251  ply1degltdimlem  34300  fedgmullem2  34308  fldextrspunlsplem  34351  constrrtll  34409  constrrtlc1  34410  constrrtcclem  34412  constrrtcc  34413  constrrecl  34447  2sqr3minply  34458  cos9thpiminplylem1  34460  cos9thpiminplylem2  34461  carsggect  34996  carsgclctunlem2  34997  ballotlemfrceq  35207  ballotlemrinv0  35211  hashreprin  35295  hgt750lemb  35331  faclimlem1  36600  irrdifflemf  38339  poimirlem4  38635  poimirlem23  38654  mblfinlem2  38669  voliunnfl  38675  volsupnfl  38676  itg2addnclem3  38684  ftc2nc  38713  dvasin  38715  areacirclem1  38719  areacirclem4  38722  rngonegmn1l  38968  rngonegmn1r  38969  lfl0  40215  latmassOLD  40379  omlmod1i2N  40410  llnexchb2lem  41018  dalawlem3  41023  pmapj2N  41079  osumcllem9N  41114  pexmidlem6N  41125  4atexlemc  41219  cdleme1  41377  cdleme42a  41621  cdlemg13a  41801  cdlemh2  41966  cdlemk1  41981  tendocnv  42171  dihmeetlem12N  42468  dihmeetlem16N  42472  dihmeetlem19N  42475  dochsatshp  42601  dochexmidlem6  42615  mapdval4N  42782  mapdpglem28  42851  mapdpglem31  42853  mapdindp4  42873  hdmap14lem1a  43016  hdmapinvlem4  43071  3rdpwhole  43442  oexpreposd  43472  remul01  43551  sn-negex12  43561  sn-subeu  43571  remulinvcom  43577  sn-0tie0  43608  cnreeu  43647  fltnlta  43767  irrapxlem5  43926  pellfund14  43998  rmxdbl  44039  jm2.22  44095  oaabsb  44389  oaun2  44476  oaun3  44477  sqrtcval  44734  0ellimcdiv  46752  fourierdlem95  47304  etransclem46  47383  sigariz  47966  sin5tlem2  48013  sin5tlem5  48016  cos5t  48018  ichreuopeq  48648  gricushgr  49108  altgsumbc  49557  blengt1fldiv2p1  49798  restclsseplem  50122  cofu1a  50302  cofu2a  50303  uobeqw  50428  swapf2fval  50480  swapf1val  50482  coccom  50940