Theorem 3eqtrrd 2779

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

Syntax hints:   → wi 4   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  fimacnvinrn  7090  fvcofneq  7112  iunfictbso  10151  axcnre  11201  fseq1p1m1  13634  seqf1olem1  14078  expmulz  14145  expubnd  14213  subsq  14245  bcm1k  14350  bcpasc  14356  cshwcshid  14862  crim  15150  rereb  15155  rlimrecl  15612  iseraltlem2  15715  fsumsplit1  15777  fsumparts  15838  isumshft  15871  geoserg  15898  pwdif  15900  efsub  16132  sincossq  16208  efieq1re  16231  nn0expgcd  16597  eucalg  16620  lcmfunsnlem  16674  phiprmpw  16809  modprmn0modprm0  16840  coprimeprodsq  16841  pythagtriplem15  16862  pythagtriplem17  16864  fldivp1  16930  1arithlem4  16959  setsidvald  17232  setsidvaldOLD  17233  setsid  17241  pwsbas  17533  invfuc  18030  estrreslem1  18191  latdisdlem  18553  ghmquskerco  19314  odinv  19593  frgpuplem  19804  gexexlem  19884  fincygsubgodd  20146  srgbinomlem4  20246  gsumdixp  20332  c0snmgmhm  20478  funcrngcsetc  20656  funcringcsetc  20690  cnfldsub  21427  mplcoe1  22072  evlsvarsrng  22140  psdmul  22187  ply1idvr1OLD  22314  ply1coe  22317  evls1varsrng  22359  mat1scmat  22560  m1detdiag  22618  mdetunilem7  22639  madugsum  22664  pm2mpmhmlem2  22840  mretopd  23115  upxp  23646  uptx  23648  imasdsf1olem  24398  clmvs2  25140  cphipipcj  25247  cphipval2  25288  itgmulc2lem2  25882  r1pid  26214  coeeulem  26277  fta1lem  26363  aaliou3lem8  26401  eff1olem  26604  tanarg  26675  logcnlem4  26701  root1cj  26813  angpieqvdlem  26885  quad2  26896  dcubic  26903  quart1  26913  jensen  27046  lgamgulmlem5  27090  lgamgulm2  27093  ftalem5  27134  basellem8  27145  chpchtsum  27277  logfaclbnd  27280  perfectlem2  27288  gausslemma2dlem1a  27423  2sqlem3  27478  dchrvmasum2lem  27554  dchrvmasumiflem2  27560  selberglem2  27604  selberg3r  27627  pntlem3  27667  ostth2  27695  ostth3  27696  madeoldsuc  27937  zseo  28420  addhalfcut  28433  krippenlem  28712  colinearalglem1  28935  axlowdimlem16  28986  axcontlem4  28996  clwlkclwwlkfo  30037  nmbdoplbi  32052  nmcopexi  32055  nmbdfnlbi  32077  nmcfnexi  32079  nmcfnlbi  32080  hstoh  32260  fcobij  32739  lt2addrd  32761  xlt2addrd  32768  cshwrnid  32930  symgfcoeu  33084  cycpmconjslem2  33157  cycpmconjs  33158  isarchi3  33176  archirngz  33178  elrspunsn  33436  mxidlirredi  33478  1arithidomlem1  33542  1arithidomlem2  33543  1arithidom  33544  dimkerim  33654  lvecendof1f1o  33660  2sqr3minply  33752  submatminr1  33770  mdetpmtr1  33783  madjusmdetlem1  33787  zarcmplem  33841  qqhnm  33952  esumfzf  34049  ddemeas  34216  sseqp1  34376  ballotlemi1  34483  ballotlemii  34484  ballotlemic  34487  ballotlem1c  34488  fsum2dsub  34600  circlemeth  34633  hgt750lemb  34649  hgt750lema  34650  hgt750leme  34651  elmrsubrn  35504  cos2h  37597  itg2addnclem  37657  itgmulc2nclem2  37673  areacirclem1  37694  areacirclem4  37697  cntotbnd  37782  atmod2i2  39844  trljat1  40148  trljat2  40149  cdleme9  40235  cdleme15b  40257  cdleme20c  40293  cdleme22eALTN  40327  dvhopN  41098  doca2N  41108  cdlemn10  41188  dochocss  41348  djhlj  41383  dihprrnlem1N  41406  dihprrnlem2  41407  lcfl7lem  41481  lclkrlem2c  41491  hgmapadd  41876  hdmapinvlem3  41902  hgmapvvlem1  41905  sumcubes  42325  zaddcomlem  42457  fidomncyc  42521  selvvvval  42571  rmydbl  42928  jm2.18  42976  jm2.19  42981  proot1hash  43183  dssmapnvod  44009  binomcxplemnotnn0  44351  oddfl  45227  dstregt0  45231  supsubc  45302  absimlere  45429  uzinico2  45514  mccllem  45552  ellimcabssub0  45572  sumnnodd  45585  climresmpt  45614  limsupresuz  45658  liminfresuz  45739  coskpi2  45821  cosknegpi  45824  dvsinax  45868  dvnmptdivc  45893  dvnxpaek  45897  dvnmul  45898  dvmptfprodlem  45899  ditgeqiooicc  45915  itgioocnicc  45932  itgspltprt  45934  wallispi2lem2  46027  dirkerper  46051  dirkertrigeqlem2  46054  dirkertrigeqlem3  46055  dirkertrigeq  46056  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem18  46080  fourierdlem19  46081  fourierdlem33  46095  fourierdlem35  46097  fourierdlem41  46103  fourierdlem42  46104  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem53  46114  fourierdlem63  46124  fourierdlem65  46126  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem81  46142  fourierdlem82  46143  fourierdlem83  46144  fourierdlem84  46145  fourierdlem90  46151  fourierdlem93  46154  fourierdlem95  46156  fourierdlem103  46164  fourierdlem104  46165  fourierdlem107  46168  fourierdlem111  46172  fourierswlem  46185  fouriersw  46186  etransclem4  46193  etransclem9  46198  etransclem28  46217  etransclem35  46224  etransclem38  46227  sge0tsms  46335  sge0sup  46346  sge0resplit  46361  sge0split  46364  sge0ss  46367  sge0rpcpnf  46376  sge0isum  46382  sge0xadd  46390  sge0seq  46401  ismeannd  46422  caratheodorylem1  46481  isomenndlem  46485  hoicvrrex  46511  ovn0lem  46520  hoidmvlelem2  46551  hoidmvlelem3  46552  ovnlecvr2  46565  voncmpl  46576  hspmbllem1  46581  hspmbllem2  46582  ovolval4lem1  46604  incsmf  46697  smfpimltmpt  46701  smfpimltxrmptf  46713  decsmf  46722  smfpimgtmpt  46736  smfpimgtxrmptf  46739  smfmullem1  46746  smflimsuplem2  46776  sigarac  46807  cevathlem2  46823  fmtnorec3  47472  fmtnorec4  47473  oddflALTV  47587  perfectALTVlem2  47646  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  uspgrlimlem1  47890  gpgvtxedg0  47955  gpgvtxedg1  47956  ply1mulgsum  48235  lindslinindsimp2lem5  48307  m1modmmod  48370  nn0sumshdiglemA  48468  nn0sumshdiglemB  48469  nn0sumshdiglem2  48471  itschlc0yqe  48609