Theorem 3eqtrrd 2777

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  fimacnvinrn  7073  fvcofneq  7094  iunfictbso  10108  axcnre  11158  fseq1p1m1  13574  seqf1olem1  14006  expmulz  14073  expubnd  14141  subsq  14173  bcm1k  14274  bcpasc  14280  cshwcshid  14777  crim  15061  rereb  15066  rlimrecl  15523  iseraltlem2  15628  fsumsplit1  15690  fsumparts  15751  isumshft  15784  geoserg  15811  pwdif  15813  efsub  16042  sincossq  16118  efieq1re  16141  eucalg  16523  lcmfunsnlem  16577  phiprmpw  16708  modprmn0modprm0  16739  coprimeprodsq  16740  pythagtriplem15  16761  pythagtriplem17  16763  fldivp1  16829  1arithlem4  16858  setsidvald  17131  setsidvaldOLD  17132  setsid  17140  pwsbas  17432  invfuc  17926  estrreslem1  18087  latdisdlem  18448  odinv  19428  frgpuplem  19639  gexexlem  19719  fincygsubgodd  19981  srgbinomlem4  20051  gsumdixp  20130  cnfldsub  20972  mplcoe1  21591  evlsvarsrng  21661  ply1idvr1  21816  ply1coe  21819  evls1varsrng  21858  mat1scmat  22040  m1detdiag  22098  mdetunilem7  22119  madugsum  22144  pm2mpmhmlem2  22320  mretopd  22595  upxp  23126  uptx  23128  imasdsf1olem  23878  clmvs2  24609  cphipipcj  24716  cphipval2  24757  itgmulc2lem2  25349  r1pid  25676  coeeulem  25737  fta1lem  25819  aaliou3lem8  25857  eff1olem  26056  tanarg  26126  logcnlem4  26152  root1cj  26261  angpieqvdlem  26330  quad2  26341  dcubic  26348  quart1  26358  jensen  26490  lgamgulmlem5  26534  lgamgulm2  26537  ftalem5  26578  basellem8  26589  chpchtsum  26719  logfaclbnd  26722  perfectlem2  26730  gausslemma2dlem1a  26865  2sqlem3  26920  dchrvmasum2lem  26996  dchrvmasumiflem2  27002  selberglem2  27046  selberg3r  27069  pntlem3  27109  ostth2  27137  ostth3  27138  madeoldsuc  27376  krippenlem  27938  colinearalglem1  28161  axlowdimlem16  28212  axcontlem4  28222  clwlkclwwlkfo  29259  nmbdoplbi  31272  nmcopexi  31275  nmbdfnlbi  31297  nmcfnexi  31299  nmcfnlbi  31300  hstoh  31480  fcobij  31942  lt2addrd  31959  xlt2addrd  31966  cshwrnid  32120  symgfcoeu  32238  cycpmconjslem2  32309  cycpmconjs  32310  isarchi3  32328  archirngz  32330  ghmquskerco  32524  elrspunsn  32542  mxidlirredi  32582  dimkerim  32707  submatminr1  32785  mdetpmtr1  32798  madjusmdetlem1  32802  zarcmplem  32856  qqhnm  32965  esumfzf  33062  ddemeas  33229  sseqp1  33389  ballotlemi1  33496  ballotlemii  33497  ballotlemic  33500  ballotlem1c  33501  fsum2dsub  33614  circlemeth  33647  hgt750lemb  33663  hgt750lema  33664  hgt750leme  33665  elmrsubrn  34506  cos2h  36474  itg2addnclem  36534  itgmulc2nclem2  36550  areacirclem1  36571  areacirclem4  36574  cntotbnd  36659  atmod2i2  38728  trljat1  39032  trljat2  39033  cdleme9  39119  cdleme15b  39141  cdleme20c  39177  cdleme22eALTN  39211  dvhopN  39982  doca2N  39992  cdlemn10  40072  dochocss  40232  djhlj  40267  dihprrnlem1N  40290  dihprrnlem2  40291  lcfl7lem  40365  lclkrlem2c  40375  hgmapadd  40760  hdmapinvlem3  40786  hgmapvvlem1  40789  selvvvval  41159  sumcubes  41211  nn0expgcd  41226  zaddcomlem  41325  rmydbl  41669  jm2.18  41717  jm2.19  41722  proot1hash  41932  dssmapnvod  42761  binomcxplemnotnn0  43105  oddfl  43977  dstregt0  43981  supsubc  44053  absimlere  44180  uzinico2  44265  mccllem  44303  ellimcabssub0  44323  sumnnodd  44336  climresmpt  44365  limsupresuz  44409  liminfresuz  44490  coskpi2  44572  cosknegpi  44575  dvsinax  44619  dvnmptdivc  44644  dvnxpaek  44648  dvnmul  44649  dvmptfprodlem  44650  ditgeqiooicc  44666  itgioocnicc  44683  itgspltprt  44685  wallispi2lem2  44778  dirkerper  44802  dirkertrigeqlem2  44805  dirkertrigeqlem3  44806  dirkertrigeq  44807  dirkercncflem2  44810  dirkercncflem4  44812  fourierdlem18  44831  fourierdlem19  44832  fourierdlem33  44846  fourierdlem35  44848  fourierdlem41  44854  fourierdlem42  44855  fourierdlem48  44860  fourierdlem49  44861  fourierdlem50  44862  fourierdlem53  44865  fourierdlem63  44875  fourierdlem65  44877  fourierdlem73  44885  fourierdlem74  44886  fourierdlem75  44887  fourierdlem81  44893  fourierdlem82  44894  fourierdlem83  44895  fourierdlem84  44896  fourierdlem90  44902  fourierdlem93  44905  fourierdlem95  44907  fourierdlem103  44915  fourierdlem104  44916  fourierdlem107  44919  fourierdlem111  44923  fourierswlem  44936  fouriersw  44937  etransclem4  44944  etransclem9  44949  etransclem28  44968  etransclem35  44975  etransclem38  44978  sge0tsms  45086  sge0sup  45097  sge0resplit  45112  sge0split  45115  sge0ss  45118  sge0rpcpnf  45127  sge0isum  45133  sge0xadd  45141  sge0seq  45152  ismeannd  45173  caratheodorylem1  45232  isomenndlem  45236  hoicvrrex  45262  ovn0lem  45271  hoidmvlelem2  45302  hoidmvlelem3  45303  ovnlecvr2  45316  voncmpl  45327  hspmbllem1  45332  hspmbllem2  45333  ovolval4lem1  45355  incsmf  45448  smfpimltmpt  45452  smfpimltxrmptf  45464  decsmf  45473  smfpimgtmpt  45487  smfpimgtxrmptf  45490  smfmullem1  45497  smfinfmpt  45525  smflimsuplem2  45527  sigarac  45558  cevathlem2  45574  fmtnorec3  46206  fmtnorec4  46207  oddflALTV  46321  perfectALTVlem2  46380  nnsum4primeseven  46458  nnsum4primesevenALTV  46459  c0snmgmhm  46703  funcrngcsetc  46886  funcringcsetc  46923  ply1mulgsum  47061  lindslinindsimp2lem5  47133  m1modmmod  47197  nn0sumshdiglemA  47295  nn0sumshdiglemB  47296  nn0sumshdiglem2  47298  itschlc0yqe  47436