Theorem 3eqtrrd 2775

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 2770	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtrd.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2771	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 2707

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

This theorem is referenced by:  fimacnvinrn  7060  fvcofneq  7082  iunfictbso  10126  axcnre  11176  fseq1p1m1  13613  seqf1olem1  14057  expmulz  14124  expubnd  14194  subsq  14226  bcm1k  14331  bcpasc  14337  cshwcshid  14844  crim  15132  rereb  15137  rlimrecl  15594  iseraltlem2  15697  fsumsplit1  15759  fsumparts  15820  isumshft  15853  geoserg  15880  pwdif  15882  efsub  16116  sincossq  16192  efieq1re  16215  nn0expgcd  16581  eucalg  16604  lcmfunsnlem  16658  phiprmpw  16793  modprmn0modprm0  16825  coprimeprodsq  16826  pythagtriplem15  16847  pythagtriplem17  16849  fldivp1  16915  1arithlem4  16944  setsidvald  17216  setsid  17224  pwsbas  17499  invfuc  17988  estrreslem1  18147  latdisdlem  18504  ghmquskerco  19265  odinv  19540  frgpuplem  19751  gexexlem  19831  fincygsubgodd  20093  srgbinomlem4  20187  gsumdixp  20277  c0snmgmhm  20420  funcrngcsetc  20598  funcringcsetc  20632  cnfldsub  21358  mplcoe1  21993  evlsvarsrng  22055  psdmul  22102  ply1idvr1OLD  22231  ply1coe  22234  evls1varsrng  22276  mat1scmat  22475  m1detdiag  22533  mdetunilem7  22554  madugsum  22579  pm2mpmhmlem2  22755  mretopd  23028  upxp  23559  uptx  23561  imasdsf1olem  24310  clmvs2  25043  cphipipcj  25150  cphipval2  25191  itgmulc2lem2  25784  r1pid  26116  coeeulem  26179  fta1lem  26265  aaliou3lem8  26303  eff1olem  26507  tanarg  26578  logcnlem4  26604  root1cj  26716  angpieqvdlem  26788  quad2  26799  dcubic  26806  quart1  26816  jensen  26949  lgamgulmlem5  26993  lgamgulm2  26996  ftalem5  27037  basellem8  27048  chpchtsum  27180  logfaclbnd  27183  perfectlem2  27191  gausslemma2dlem1a  27326  2sqlem3  27381  dchrvmasum2lem  27457  dchrvmasumiflem2  27463  selberglem2  27507  selberg3r  27530  pntlem3  27570  ostth2  27598  ostth3  27599  madeoldsuc  27840  zseo  28323  addhalfcut  28336  krippenlem  28615  colinearalglem1  28831  axlowdimlem16  28882  axcontlem4  28892  clwlkclwwlkfo  29936  nmbdoplbi  31951  nmcopexi  31954  nmbdfnlbi  31976  nmcfnexi  31978  nmcfnlbi  31979  hstoh  32159  fcobij  32645  lt2addrd  32674  xlt2addrd  32682  cshwrnid  32883  symgfcoeu  33039  cycpmconjslem2  33112  cycpmconjs  33113  isarchi3  33131  archirngz  33133  elrgspnsubrunlem1  33188  elrspunsn  33390  mxidlirredi  33432  1arithidomlem1  33496  1arithidomlem2  33497  1arithidom  33498  dimkerim  33613  lvecendof1f1o  33619  fldextrspunlsplem  33660  nn0constr  33741  constraddcl  33742  constrnegcl  33743  constrremulcl  33747  constrrecl  33749  constrimcl  33750  constrmulcl  33751  constrreinvcl  33752  constrinvcl  33753  constrresqrtcl  33757  constrabscl  33758  2sqr3minply  33760  submatminr1  33787  mdetpmtr1  33800  madjusmdetlem1  33804  zarcmplem  33858  qqhnm  33967  esumfzf  34046  ddemeas  34213  sseqp1  34373  ballotlemi1  34481  ballotlemii  34482  ballotlemic  34485  ballotlem1c  34486  fsum2dsub  34585  circlemeth  34618  hgt750lemb  34634  hgt750lema  34635  hgt750leme  34636  elmrsubrn  35488  cos2h  37581  itg2addnclem  37641  itgmulc2nclem2  37657  areacirclem1  37678  areacirclem4  37681  cntotbnd  37766  atmod2i2  39827  trljat1  40131  trljat2  40132  cdleme9  40218  cdleme15b  40240  cdleme20c  40276  cdleme22eALTN  40310  dvhopN  41081  doca2N  41091  cdlemn10  41171  dochocss  41331  djhlj  41366  dihprrnlem1N  41389  dihprrnlem2  41390  lcfl7lem  41464  lclkrlem2c  41474  hgmapadd  41859  hdmapinvlem3  41885  hgmapvvlem1  41888  sumcubes  42309  zaddcomlem  42441  fidomncyc  42505  selvvvval  42555  rmydbl  42911  jm2.18  42959  jm2.19  42964  proot1hash  43166  dssmapnvod  43991  binomcxplemnotnn0  44328  oddfl  45254  dstregt0  45258  supsubc  45328  absimlere  45454  uzinico2  45538  mccllem  45574  ellimcabssub0  45594  sumnnodd  45607  climresmpt  45636  limsupresuz  45680  liminfresuz  45761  coskpi2  45843  cosknegpi  45846  dvsinax  45890  dvnmptdivc  45915  dvnxpaek  45919  dvnmul  45920  dvmptfprodlem  45921  ditgeqiooicc  45937  itgioocnicc  45954  itgspltprt  45956  wallispi2lem2  46049  dirkerper  46073  dirkertrigeqlem2  46076  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem18  46102  fourierdlem19  46103  fourierdlem33  46117  fourierdlem35  46119  fourierdlem41  46125  fourierdlem42  46126  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem53  46136  fourierdlem63  46146  fourierdlem65  46148  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem81  46164  fourierdlem82  46165  fourierdlem83  46166  fourierdlem84  46167  fourierdlem90  46173  fourierdlem93  46176  fourierdlem95  46178  fourierdlem103  46186  fourierdlem104  46187  fourierdlem107  46190  fourierdlem111  46194  fourierswlem  46207  fouriersw  46208  etransclem4  46215  etransclem9  46220  etransclem28  46239  etransclem35  46246  etransclem38  46249  sge0tsms  46357  sge0sup  46368  sge0resplit  46383  sge0split  46386  sge0ss  46389  sge0rpcpnf  46398  sge0isum  46404  sge0xadd  46412  sge0seq  46423  ismeannd  46444  caratheodorylem1  46503  isomenndlem  46507  hoicvrrex  46533  ovn0lem  46542  hoidmvlelem2  46573  hoidmvlelem3  46574  ovnlecvr2  46587  voncmpl  46598  hspmbllem1  46603  hspmbllem2  46604  ovolval4lem1  46626  incsmf  46719  smfpimltmpt  46723  smfpimltxrmptf  46735  decsmf  46744  smfpimgtmpt  46758  smfpimgtxrmptf  46761  smfmullem1  46768  smflimsuplem2  46798  sigarac  46829  cevathlem2  46845  fmtnorec3  47510  fmtnorec4  47511  oddflALTV  47625  perfectALTVlem2  47684  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  uspgrlimlem1  47948  gpgvtxedg0  48015  gpgvtxedg1  48016  gpg3kgrtriexlem2  48034  ply1mulgsum  48314  lindslinindsimp2lem5  48386  m1modmmod  48449  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548  nn0sumshdiglem2  48550  itschlc0yqe  48688