Theorem 3eqtr3rd 2863

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

Syntax hints:   → wi 4   = wceq 1531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-cleq 2812

This theorem is referenced by:  iunxdif3  5008  fcofo  7036  fcof1oinvd  7041  cantnfp1lem3  9135  fin1a2lem7  9820  prlem934  10447  addid2  10815  addcom  10818  addcomd  10834  negeu  10868  add20  11144  2halves  11857  bcnn  13664  bcpasc  13673  hashfun  13790  wrdeqs1cat  14074  sqreulem  14711  summolem3  15063  fsumneg  15134  geolim  15218  geolim2  15219  mertens  15234  prodmolem3  15279  fallrisefac  15371  bpoly3  15404  sincossq  15521  demoivre  15545  eirrlem  15549  oddpwp1fsum  15735  sadeq  15813  gcdid  15867  gcdmultipled  15874  phiprmpw  16105  pythagtriplem12  16155  expnprm  16230  fullresc  17113  grpinvid1  18146  grpnpcan  18183  grplactcnv  18194  ghmgrp  18215  conjghm  18381  odmodnn0  18660  gex1  18708  sylow3lem3  18746  efgredeu  18870  odadd2  18961  gsumval3  19019  pgpfac1lem3a  19190  ringnegl  19336  rngnegr  19337  ringmneg2  19339  lmodfopne  19664  lmodvsneg  19670  lss0v  19780  lssvs0or  19874  lvecinv  19877  lspabs2  19884  mplcoe3  20239  mplcoe5  20241  evlvar  20305  zringunit  20627  zringcyg  20630  mdetrlin  21203  mdetunilem6  21218  cramerimplem3  21286  cramerimp  21287  paste  21894  tuslem  22868  tususs  22871  ngpds  23205  ioo2bl  23393  ipcau2  23829  dvexp3  24567  rolle  24579  cmvth  24580  dv11cn  24590  lhop  24605  itgsubstlem  24637  ply1divex  24722  fta1glem1  24751  fta1g  24753  dgrnznn  24829  fta1  24889  vieta1lem2  24892  aaliou2  24921  dvtaylp  24950  dvntaylp  24951  taylthlem1  24953  taylthlem2  24954  dvradcnv  25001  ptolemy  25074  coskpi  25100  tanregt0  25115  cxpeq  25330  isosctrlem2  25389  chordthmlem  25402  dcubic  25416  quart1lem  25425  tanatan  25489  atantan  25493  dvatan  25505  birthdaylem2  25522  rlimcxp  25543  jensenlem2  25557  logdiflbnd  25564  emcllem2  25566  lgamgulmlem2  25599  lgamcvg2  25624  basellem8  25657  bclbnd  25848  lgsqr  25919  lgseisenlem3  25945  lgseisenlem4  25946  lgsquadlem1  25948  lgsquadlem2  25949  rpvmasumlem  26055  dchrisumlem1  26057  dchrisum0flblem1  26076  dchrisum0flblem2  26077  dchrisum0re  26081  dchrisum0lem1  26084  mudivsum  26098  mulogsum  26100  vmalogdivsum2  26106  logsqvma2  26111  selberg2lem  26118  logdivbnd  26124  selbergr  26136  selberg3r  26137  pntrlog2bndlem4  26148  pntrlog2bndlem5  26149  pntpbnd2  26155  miduniq  26463  krippenlem  26468  colperpexlem2  26509  ttgcontlem1  26663  brbtwn2  26683  colinearalglem4  26687  axsegconlem9  26703  ax5seglem1  26706  axbtwnid  26717  axeuclidlem  26740  axcontlem2  26743  axcontlem4  26745  grpoinvid1  28297  vcz  28344  hosubsub4  29587  lnop0  29735  branmfn  29874  difico  30498  wrdsplex  30607  s3f1  30616  ccatf1  30618  omndmul2  30706  cycpmco2lem4  30764  tocyccntz  30779  cyc3genpm  30787  cycpmconjslem2  30790  dvdschrmulg  30851  rdivmuldivd  30855  kerunit  30889  qustrivr  30923  linds2eq  30934  fedgmullem2  31019  carsggect  31569  carsgclctunlem2  31570  ballotlemfrceq  31779  ballotlemrinv0  31783  hashreprin  31884  hgt750lemb  31920  hashf1dmrn  32348  faclimlem1  32968  poimirlem4  34888  poimirlem23  34907  mblfinlem2  34922  voliunnfl  34928  volsupnfl  34929  itg2addnclem3  34937  ftc2nc  34968  dvasin  34970  areacirclem1  34974  areacirclem4  34977  rngonegmn1l  35211  rngonegmn1r  35212  lfl0  36193  latmassOLD  36357  omlmod1i2N  36388  llnexchb2lem  36996  dalawlem3  37001  pmapj2N  37057  osumcllem9N  37092  pexmidlem6N  37103  4atexlemc  37197  cdleme1  37355  cdleme42a  37599  cdlemg13a  37779  cdlemh2  37944  cdlemk1  37959  tendocnv  38149  dihmeetlem12N  38446  dihmeetlem16N  38450  dihmeetlem19N  38453  dochsatshp  38579  dochexmidlem6  38593  mapdval4N  38760  mapdpglem28  38829  mapdpglem31  38831  mapdindp4  38851  hdmap14lem1a  38994  hdmapinvlem4  39049  oexpreposd  39170  nn0rppwr  39173  sn-00idlem3  39221  remul01  39228  remulinvcom  39239  fltnlta  39266  irrapxlem5  39414  pellfund14  39486  rmxdbl  39527  jm2.22  39583  itgpowd  39812  0ellimcdiv  41920  fourierdlem95  42477  etransclem46  42556  sigariz  43111  ichreuopeq  43626  isomushgr  43982  altgsumbc  44391  blengt1fldiv2p1  44644