Theorem 3eqtr3rd 2868

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

Syntax hints:   → wi 4   = wceq 1536

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 1969  ax-7 2014  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817

This theorem is referenced by:  iunxdif3  5020  fcofo  7047  fcof1oinvd  7052  cantnfp1lem3  9146  fin1a2lem7  9831  prlem934  10458  addid2  10826  addcom  10829  addcomd  10845  negeu  10879  add20  11155  2halves  11868  bcnn  13675  bcpasc  13684  hashfun  13801  wrdeqs1cat  14085  sqreulem  14722  summolem3  15074  fsumneg  15145  geolim  15229  geolim2  15230  mertens  15245  prodmolem3  15290  fallrisefac  15382  bpoly3  15415  sincossq  15532  demoivre  15556  eirrlem  15560  oddpwp1fsum  15746  sadeq  15824  gcdid  15878  gcdmultipled  15885  phiprmpw  16116  pythagtriplem12  16166  expnprm  16241  fullresc  17124  grpinvid1  18157  grpnpcan  18194  grplactcnv  18205  ghmgrp  18226  conjghm  18392  odmodnn0  18671  gex1  18719  sylow3lem3  18757  efgredeu  18881  odadd2  18972  gsumval3  19030  pgpfac1lem3a  19201  ringnegl  19347  rngnegr  19348  ringmneg2  19350  lmodfopne  19675  lmodvsneg  19681  lss0v  19791  lssvs0or  19885  lvecinv  19888  lspabs2  19895  mplcoe3  20250  mplcoe5  20252  evlvar  20316  zringunit  20638  zringcyg  20641  mdetrlin  21214  mdetunilem6  21229  cramerimplem3  21297  cramerimp  21298  paste  21905  tuslem  22879  tususs  22882  ngpds  23216  ioo2bl  23404  ipcau2  23840  dvexp3  24578  rolle  24590  cmvth  24591  dv11cn  24601  lhop  24616  itgsubstlem  24648  ply1divex  24733  fta1glem1  24762  fta1g  24764  dgrnznn  24840  fta1  24900  vieta1lem2  24903  aaliou2  24932  dvtaylp  24961  dvntaylp  24962  taylthlem1  24964  taylthlem2  24965  dvradcnv  25012  ptolemy  25085  coskpi  25111  tanregt0  25126  cxpeq  25341  isosctrlem2  25400  chordthmlem  25413  dcubic  25427  quart1lem  25436  tanatan  25500  atantan  25504  dvatan  25516  birthdaylem2  25533  rlimcxp  25554  jensenlem2  25568  logdiflbnd  25575  emcllem2  25577  lgamgulmlem2  25610  lgamcvg2  25635  basellem8  25668  bclbnd  25859  lgsqr  25930  lgseisenlem3  25956  lgseisenlem4  25957  lgsquadlem1  25959  lgsquadlem2  25960  rpvmasumlem  26066  dchrisumlem1  26068  dchrisum0flblem1  26087  dchrisum0flblem2  26088  dchrisum0re  26092  dchrisum0lem1  26095  mudivsum  26109  mulogsum  26111  vmalogdivsum2  26117  logsqvma2  26122  selberg2lem  26129  logdivbnd  26135  selbergr  26147  selberg3r  26148  pntrlog2bndlem4  26159  pntrlog2bndlem5  26160  pntpbnd2  26166  miduniq  26474  krippenlem  26479  colperpexlem2  26520  ttgcontlem1  26674  brbtwn2  26694  colinearalglem4  26698  axsegconlem9  26714  ax5seglem1  26717  axbtwnid  26728  axeuclidlem  26751  axcontlem2  26754  axcontlem4  26756  grpoinvid1  28308  vcz  28355  hosubsub4  29598  lnop0  29746  branmfn  29885  difico  30509  wrdsplex  30618  s3f1  30627  ccatf1  30629  omndmul2  30717  cycpmco2lem4  30775  tocyccntz  30790  cyc3genpm  30798  cycpmconjslem2  30801  dvdschrmulg  30862  rdivmuldivd  30866  kerunit  30900  qustrivr  30934  linds2eq  30945  fedgmullem2  31030  carsggect  31580  carsgclctunlem2  31581  ballotlemfrceq  31790  ballotlemrinv0  31794  hashreprin  31895  hgt750lemb  31931  hashf1dmrn  32359  faclimlem1  32979  poimirlem4  34900  poimirlem23  34919  mblfinlem2  34934  voliunnfl  34940  volsupnfl  34941  itg2addnclem3  34949  ftc2nc  34980  dvasin  34982  areacirclem1  34986  areacirclem4  34989  rngonegmn1l  35223  rngonegmn1r  35224  lfl0  36205  latmassOLD  36369  omlmod1i2N  36400  llnexchb2lem  37008  dalawlem3  37013  pmapj2N  37069  osumcllem9N  37104  pexmidlem6N  37115  4atexlemc  37209  cdleme1  37367  cdleme42a  37611  cdlemg13a  37791  cdlemh2  37956  cdlemk1  37971  tendocnv  38161  dihmeetlem12N  38458  dihmeetlem16N  38462  dihmeetlem19N  38465  dochsatshp  38591  dochexmidlem6  38605  mapdval4N  38772  mapdpglem28  38841  mapdpglem31  38843  mapdindp4  38863  hdmap14lem1a  39006  hdmapinvlem4  39061  oexpreposd  39185  nn0rppwr  39188  sn-00idlem3  39236  remul01  39243  remulinvcom  39254  fltnlta  39281  irrapxlem5  39429  pellfund14  39501  rmxdbl  39542  jm2.22  39598  itgpowd  39827  0ellimcdiv  41936  fourierdlem95  42493  etransclem46  42572  sigariz  43127  ichreuopeq  43642  isomushgr  43998  altgsumbc  44407  blengt1fldiv2p1  44660