Theorem 3eqtrrd 2770

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 2765	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtrd.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2766	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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  fimacnvinrn  7046  fvcofneq  7068  iunfictbso  10074  axcnre  11124  fseq1p1m1  13566  seqf1olem1  14013  expmulz  14080  expubnd  14150  subsq  14182  bcm1k  14287  bcpasc  14293  cshwcshid  14800  crim  15088  rereb  15093  rlimrecl  15553  iseraltlem2  15656  fsumsplit1  15718  fsumparts  15779  isumshft  15812  geoserg  15839  pwdif  15841  efsub  16075  sincossq  16151  efieq1re  16174  nn0expgcd  16541  eucalg  16564  lcmfunsnlem  16618  phiprmpw  16753  modprmn0modprm0  16785  coprimeprodsq  16786  pythagtriplem15  16807  pythagtriplem17  16809  fldivp1  16875  1arithlem4  16904  setsidvald  17176  setsid  17184  pwsbas  17457  invfuc  17946  estrreslem1  18105  latdisdlem  18462  ghmquskerco  19223  odinv  19498  frgpuplem  19709  gexexlem  19789  fincygsubgodd  20051  srgbinomlem4  20145  gsumdixp  20235  c0snmgmhm  20378  funcrngcsetc  20556  funcringcsetc  20590  cnfldsub  21316  mplcoe1  21951  evlsvarsrng  22013  psdmul  22060  ply1idvr1OLD  22189  ply1coe  22192  evls1varsrng  22234  mat1scmat  22433  m1detdiag  22491  mdetunilem7  22512  madugsum  22537  pm2mpmhmlem2  22713  mretopd  22986  upxp  23517  uptx  23519  imasdsf1olem  24268  clmvs2  25001  cphipipcj  25107  cphipval2  25148  itgmulc2lem2  25741  r1pid  26073  coeeulem  26136  fta1lem  26222  aaliou3lem8  26260  eff1olem  26464  tanarg  26535  logcnlem4  26561  root1cj  26673  angpieqvdlem  26745  quad2  26756  dcubic  26763  quart1  26773  jensen  26906  lgamgulmlem5  26950  lgamgulm2  26953  ftalem5  26994  basellem8  27005  chpchtsum  27137  logfaclbnd  27140  perfectlem2  27148  gausslemma2dlem1a  27283  2sqlem3  27338  dchrvmasum2lem  27414  dchrvmasumiflem2  27420  selberglem2  27464  selberg3r  27487  pntlem3  27527  ostth2  27555  ostth3  27556  madeoldsuc  27803  zseo  28315  addhalfcut  28341  krippenlem  28624  colinearalglem1  28840  axlowdimlem16  28891  axcontlem4  28901  clwlkclwwlkfo  29945  nmbdoplbi  31960  nmcopexi  31963  nmbdfnlbi  31985  nmcfnexi  31987  nmcfnlbi  31988  hstoh  32168  fcobij  32652  lt2addrd  32681  xlt2addrd  32689  cshwrnid  32890  symgfcoeu  33046  cycpmconjslem2  33119  cycpmconjs  33120  isarchi3  33148  archirngz  33150  elrgspnsubrunlem1  33205  elrspunsn  33407  mxidlirredi  33449  1arithidomlem1  33513  1arithidomlem2  33514  1arithidom  33515  dimkerim  33630  lvecendof1f1o  33636  fldextrspunlsplem  33675  nn0constr  33758  constraddcl  33759  constrnegcl  33760  constrremulcl  33764  constrrecl  33766  constrimcl  33767  constrmulcl  33768  constrreinvcl  33769  constrinvcl  33770  constrresqrtcl  33774  constrabscl  33775  2sqr3minply  33777  submatminr1  33807  mdetpmtr1  33820  madjusmdetlem1  33824  zarcmplem  33878  qqhnm  33987  esumfzf  34066  ddemeas  34233  sseqp1  34393  ballotlemi1  34501  ballotlemii  34502  ballotlemic  34505  ballotlem1c  34506  fsum2dsub  34605  circlemeth  34638  hgt750lemb  34654  hgt750lema  34655  hgt750leme  34656  elmrsubrn  35514  cos2h  37612  itg2addnclem  37672  itgmulc2nclem2  37688  areacirclem1  37709  areacirclem4  37712  cntotbnd  37797  atmod2i2  39863  trljat1  40167  trljat2  40168  cdleme9  40254  cdleme15b  40276  cdleme20c  40312  cdleme22eALTN  40346  dvhopN  41117  doca2N  41127  cdlemn10  41207  dochocss  41367  djhlj  41402  dihprrnlem1N  41425  dihprrnlem2  41426  lcfl7lem  41500  lclkrlem2c  41510  hgmapadd  41895  hdmapinvlem3  41921  hgmapvvlem1  41924  sumcubes  42308  zaddcomlem  42458  fidomncyc  42530  selvvvval  42580  rmydbl  42936  jm2.18  42984  jm2.19  42989  proot1hash  43191  dssmapnvod  44016  binomcxplemnotnn0  44352  oddfl  45283  dstregt0  45287  supsubc  45356  absimlere  45482  uzinico2  45566  mccllem  45602  ellimcabssub0  45622  sumnnodd  45635  climresmpt  45664  limsupresuz  45708  liminfresuz  45789  coskpi2  45871  cosknegpi  45874  dvsinax  45918  dvnmptdivc  45943  dvnxpaek  45947  dvnmul  45948  dvmptfprodlem  45949  ditgeqiooicc  45965  itgioocnicc  45982  itgspltprt  45984  wallispi2lem2  46077  dirkerper  46101  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem18  46130  fourierdlem19  46131  fourierdlem33  46145  fourierdlem35  46147  fourierdlem41  46153  fourierdlem42  46154  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem53  46164  fourierdlem63  46174  fourierdlem65  46176  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem81  46192  fourierdlem82  46193  fourierdlem83  46194  fourierdlem84  46195  fourierdlem90  46201  fourierdlem93  46204  fourierdlem95  46206  fourierdlem103  46214  fourierdlem104  46215  fourierdlem107  46218  fourierdlem111  46222  fourierswlem  46235  fouriersw  46236  etransclem4  46243  etransclem9  46248  etransclem28  46267  etransclem35  46274  etransclem38  46277  sge0tsms  46385  sge0sup  46396  sge0resplit  46411  sge0split  46414  sge0ss  46417  sge0rpcpnf  46426  sge0isum  46432  sge0xadd  46440  sge0seq  46451  ismeannd  46472  caratheodorylem1  46531  isomenndlem  46535  hoicvrrex  46561  ovn0lem  46570  hoidmvlelem2  46601  hoidmvlelem3  46602  ovnlecvr2  46615  voncmpl  46626  hspmbllem1  46631  hspmbllem2  46632  ovolval4lem1  46654  incsmf  46747  smfpimltmpt  46751  smfpimltxrmptf  46763  decsmf  46772  smfpimgtmpt  46786  smfpimgtxrmptf  46789  smfmullem1  46796  smflimsuplem2  46826  sigarac  46857  cevathlem2  46873  m1modmmod  47363  fmtnorec3  47553  fmtnorec4  47554  oddflALTV  47668  perfectALTVlem2  47727  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  uspgrlimlem1  47991  gpgvtxedg0  48058  gpgvtxedg1  48059  gpg3kgrtriexlem2  48079  ply1mulgsum  48383  lindslinindsimp2lem5  48455  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  nn0sumshdiglem2  48615  itschlc0yqe  48753