Theorem 3eqtrrd 2782

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

Ref	Expression
3eqtrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)
3eqtrd.3	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
3eqtrrd	⊢ (𝜑 → 𝐷 = 𝐴)

Proof of Theorem 3eqtrrd

Step	Hyp	Ref	Expression
1		3eqtrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	1, 2	eqtrd 2777	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtrd.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2778	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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729

This theorem is referenced by:  fimacnvinrn  7091  fvcofneq  7113  iunfictbso  10154  axcnre  11204  fseq1p1m1  13638  seqf1olem1  14082  expmulz  14149  expubnd  14217  subsq  14249  bcm1k  14354  bcpasc  14360  cshwcshid  14866  crim  15154  rereb  15159  rlimrecl  15616  iseraltlem2  15719  fsumsplit1  15781  fsumparts  15842  isumshft  15875  geoserg  15902  pwdif  15904  efsub  16136  sincossq  16212  efieq1re  16235  nn0expgcd  16601  eucalg  16624  lcmfunsnlem  16678  phiprmpw  16813  modprmn0modprm0  16845  coprimeprodsq  16846  pythagtriplem15  16867  pythagtriplem17  16869  fldivp1  16935  1arithlem4  16964  setsidvald  17236  setsid  17244  pwsbas  17532  invfuc  18022  estrreslem1  18181  latdisdlem  18541  ghmquskerco  19302  odinv  19579  frgpuplem  19790  gexexlem  19870  fincygsubgodd  20132  srgbinomlem4  20226  gsumdixp  20316  c0snmgmhm  20462  funcrngcsetc  20640  funcringcsetc  20674  cnfldsub  21410  mplcoe1  22055  evlsvarsrng  22123  psdmul  22170  ply1idvr1OLD  22299  ply1coe  22302  evls1varsrng  22344  mat1scmat  22545  m1detdiag  22603  mdetunilem7  22624  madugsum  22649  pm2mpmhmlem2  22825  mretopd  23100  upxp  23631  uptx  23633  imasdsf1olem  24383  clmvs2  25127  cphipipcj  25234  cphipval2  25275  itgmulc2lem2  25868  r1pid  26200  coeeulem  26263  fta1lem  26349  aaliou3lem8  26387  eff1olem  26590  tanarg  26661  logcnlem4  26687  root1cj  26799  angpieqvdlem  26871  quad2  26882  dcubic  26889  quart1  26899  jensen  27032  lgamgulmlem5  27076  lgamgulm2  27079  ftalem5  27120  basellem8  27131  chpchtsum  27263  logfaclbnd  27266  perfectlem2  27274  gausslemma2dlem1a  27409  2sqlem3  27464  dchrvmasum2lem  27540  dchrvmasumiflem2  27546  selberglem2  27590  selberg3r  27613  pntlem3  27653  ostth2  27681  ostth3  27682  madeoldsuc  27923  zseo  28406  addhalfcut  28419  krippenlem  28698  colinearalglem1  28921  axlowdimlem16  28972  axcontlem4  28982  clwlkclwwlkfo  30028  nmbdoplbi  32043  nmcopexi  32046  nmbdfnlbi  32068  nmcfnexi  32070  nmcfnlbi  32071  hstoh  32251  fcobij  32733  lt2addrd  32755  xlt2addrd  32762  cshwrnid  32946  symgfcoeu  33102  cycpmconjslem2  33175  cycpmconjs  33176  isarchi3  33194  archirngz  33196  elrgspnsubrunlem1  33251  elrspunsn  33457  mxidlirredi  33499  1arithidomlem1  33563  1arithidomlem2  33564  1arithidom  33565  dimkerim  33678  lvecendof1f1o  33684  fldextrspunlsplem  33723  2sqr3minply  33791  submatminr1  33809  mdetpmtr1  33822  madjusmdetlem1  33826  zarcmplem  33880  qqhnm  33991  esumfzf  34070  ddemeas  34237  sseqp1  34397  ballotlemi1  34505  ballotlemii  34506  ballotlemic  34509  ballotlem1c  34510  fsum2dsub  34622  circlemeth  34655  hgt750lemb  34671  hgt750lema  34672  hgt750leme  34673  elmrsubrn  35525  cos2h  37618  itg2addnclem  37678  itgmulc2nclem2  37694  areacirclem1  37715  areacirclem4  37718  cntotbnd  37803  atmod2i2  39864  trljat1  40168  trljat2  40169  cdleme9  40255  cdleme15b  40277  cdleme20c  40313  cdleme22eALTN  40347  dvhopN  41118  doca2N  41128  cdlemn10  41208  dochocss  41368  djhlj  41403  dihprrnlem1N  41426  dihprrnlem2  41427  lcfl7lem  41501  lclkrlem2c  41511  hgmapadd  41896  hdmapinvlem3  41922  hgmapvvlem1  41925  sumcubes  42347  zaddcomlem  42481  fidomncyc  42545  selvvvval  42595  rmydbl  42952  jm2.18  43000  jm2.19  43005  proot1hash  43207  dssmapnvod  44033  binomcxplemnotnn0  44375  oddfl  45289  dstregt0  45293  supsubc  45364  absimlere  45490  uzinico2  45575  mccllem  45612  ellimcabssub0  45632  sumnnodd  45645  climresmpt  45674  limsupresuz  45718  liminfresuz  45799  coskpi2  45881  cosknegpi  45884  dvsinax  45928  dvnmptdivc  45953  dvnxpaek  45957  dvnmul  45958  dvmptfprodlem  45959  ditgeqiooicc  45975  itgioocnicc  45992  itgspltprt  45994  wallispi2lem2  46087  dirkerper  46111  dirkertrigeqlem2  46114  dirkertrigeqlem3  46115  dirkertrigeq  46116  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem18  46140  fourierdlem19  46141  fourierdlem33  46155  fourierdlem35  46157  fourierdlem41  46163  fourierdlem42  46164  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem53  46174  fourierdlem63  46184  fourierdlem65  46186  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem81  46202  fourierdlem82  46203  fourierdlem83  46204  fourierdlem84  46205  fourierdlem90  46211  fourierdlem93  46214  fourierdlem95  46216  fourierdlem103  46224  fourierdlem104  46225  fourierdlem107  46228  fourierdlem111  46232  fourierswlem  46245  fouriersw  46246  etransclem4  46253  etransclem9  46258  etransclem28  46277  etransclem35  46284  etransclem38  46287  sge0tsms  46395  sge0sup  46406  sge0resplit  46421  sge0split  46424  sge0ss  46427  sge0rpcpnf  46436  sge0isum  46442  sge0xadd  46450  sge0seq  46461  ismeannd  46482  caratheodorylem1  46541  isomenndlem  46545  hoicvrrex  46571  ovn0lem  46580  hoidmvlelem2  46611  hoidmvlelem3  46612  ovnlecvr2  46625  voncmpl  46636  hspmbllem1  46641  hspmbllem2  46642  ovolval4lem1  46664  incsmf  46757  smfpimltmpt  46761  smfpimltxrmptf  46773  decsmf  46782  smfpimgtmpt  46796  smfpimgtxrmptf  46799  smfmullem1  46806  smflimsuplem2  46836  sigarac  46867  cevathlem2  46883  fmtnorec3  47535  fmtnorec4  47536  oddflALTV  47650  perfectALTVlem2  47709  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  uspgrlimlem1  47955  gpgvtxedg0  48021  gpgvtxedg1  48022  gpg3kgrtriexlem2  48040  ply1mulgsum  48307  lindslinindsimp2lem5  48379  m1modmmod  48442  nn0sumshdiglemA  48540  nn0sumshdiglemB  48541  nn0sumshdiglem2  48543  itschlc0yqe  48681