Theorem 3eqtr3rd 2780

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  iunxdif3  5098  fcofo  7289  fcof1oinvd  7294  cantnfp1lem3  9679  fin1a2lem7  10405  prlem934  11032  addlid  11402  addcom  11405  addcomd  11421  negeu  11455  add20  11731  2halves  12445  bcnn  14277  bcpasc  14286  hashfun  14402  hashf1dmrn  14408  wrdeqs1cat  14675  sqreulem  15311  summolem3  15665  fsumneg  15738  geolim  15821  geolim2  15822  mertens  15837  prodmolem3  15882  fallrisefac  15974  bpoly3  16007  sincossq  16124  demoivre  16148  eirrlem  16152  oddpwp1fsum  16340  sadeq  16418  gcdid  16473  gcdmultipled  16481  phiprmpw  16714  pythagtriplem12  16764  expnprm  16840  fullresc  17806  grpinvid1  18913  grpnpcan  18952  grplactcnv  18963  ghmgrp  18986  conjghm  19164  odmodnn0  19450  gex1  19501  sylow3lem3  19539  efgredeu  19662  odadd2  19759  gsumval3  19817  pgpfac1lem3a  19988  ringnegl  20191  ringnegr  20192  ringmneg2  20194  rdivmuldivd  20305  imadrhmcl  20557  lmodfopne  20655  lmodvsneg  20661  lss0v  20772  lssvs0or  20869  lvecinv  20872  lspabs2  20879  zringunit  21238  zringcyg  21241  sraassab  21642  mplcoe3  21813  mplcoe5  21815  evlvar  21883  mdetrlin  22325  mdetunilem6  22340  cramerimplem3  22408  cramerimp  22409  paste  23019  tuslem  23992  tuslemOLD  23993  tususs  23996  ngpds  24334  ioo2bl  24530  ipcau2  24983  dvexp3  25731  rolle  25743  cmvth  25744  dv11cn  25754  lhop  25769  itgsubstlem  25801  itgpowd  25803  ply1divex  25890  fta1glem1  25919  fta1g  25921  dgrnznn  25997  fta1  26058  vieta1lem2  26061  aaliou2  26090  dvtaylp  26119  dvntaylp  26120  taylthlem1  26122  taylthlem2  26123  dvradcnv  26170  ptolemy  26243  coskpi  26269  tanregt0  26285  cxpeq  26502  isosctrlem2  26561  chordthmlem  26574  dcubic  26588  quart1lem  26597  tanatan  26661  atantan  26665  dvatan  26677  birthdaylem2  26694  rlimcxp  26715  jensenlem2  26729  logdiflbnd  26736  emcllem2  26738  lgamgulmlem2  26771  lgamcvg2  26796  basellem8  26829  bclbnd  27020  lgsqr  27091  lgseisenlem3  27117  lgseisenlem4  27118  lgsquadlem1  27120  lgsquadlem2  27121  rpvmasumlem  27227  dchrisumlem1  27229  dchrisum0flblem1  27248  dchrisum0flblem2  27249  dchrisum0re  27253  dchrisum0lem1  27256  mudivsum  27270  mulogsum  27272  vmalogdivsum2  27278  logsqvma2  27283  selberg2lem  27290  logdivbnd  27296  selbergr  27308  selberg3r  27309  pntrlog2bndlem4  27320  pntrlog2bndlem5  27321  pntpbnd2  27327  miduniq  28204  krippenlem  28209  colperpexlem2  28250  ttgcontlem1  28410  brbtwn2  28431  colinearalglem4  28435  axsegconlem9  28451  ax5seglem1  28454  axbtwnid  28465  axeuclidlem  28488  axcontlem2  28491  axcontlem4  28493  grpoinvid1  30049  vcz  30096  hosubsub4  31339  lnop0  31487  branmfn  31626  fressupp  32178  difico  32262  wrdsplex  32372  s3f1  32381  ccatf1  32383  mgcf1o  32441  omndmul2  32501  cycpmco2lem4  32559  tocyccntz  32574  cyc3genpm  32582  cycpmconjslem2  32585  dvdschrmulg  32651  kerunit  32708  qustrivr  32752  fermltlchr  32753  znfermltl  32754  dvdsruassoi  32764  dvdsruasso  32765  linds2eq  32772  qsdrnglem2  32885  ply1degltdimlem  32996  fedgmullem2  33004  carsggect  33616  carsgclctunlem2  33617  ballotlemfrceq  33826  ballotlemrinv0  33830  hashreprin  33931  hgt750lemb  33967  faclimlem1  35018  gg-cmvth  35467  irrdifflemf  36510  poimirlem4  36796  poimirlem23  36815  mblfinlem2  36830  voliunnfl  36836  volsupnfl  36837  itg2addnclem3  36845  ftc2nc  36874  dvasin  36876  areacirclem1  36880  areacirclem4  36883  rngonegmn1l  37113  rngonegmn1r  37114  lfl0  38239  latmassOLD  38403  omlmod1i2N  38434  llnexchb2lem  39043  dalawlem3  39048  pmapj2N  39104  osumcllem9N  39139  pexmidlem6N  39150  4atexlemc  39244  cdleme1  39402  cdleme42a  39646  cdlemg13a  39826  cdlemh2  39991  cdlemk1  40006  tendocnv  40196  dihmeetlem12N  40493  dihmeetlem16N  40497  dihmeetlem19N  40500  dochsatshp  40626  dochexmidlem6  40640  mapdval4N  40807  mapdpglem28  40876  mapdpglem31  40878  mapdindp4  40898  hdmap14lem1a  41041  hdmapinvlem4  41096  oexpreposd  41515  nn0rppwr  41527  sn-00idlem3  41576  remul01  41583  sn-subeu  41602  remulinvcom  41608  sn-0tie0  41615  cnreeu  41644  fltnlta  41708  irrapxlem5  41867  pellfund14  41939  rmxdbl  41981  jm2.22  42037  oaabsb  42347  oaun2  42434  oaun3  42435  sqrtcval  42695  0ellimcdiv  44664  fourierdlem95  45216  etransclem46  45295  sigariz  45878  ichreuopeq  46440  isomushgr  46793  altgsumbc  47117  blengt1fldiv2p1  47367  restclsseplem  47635