Theorem 3eqtrrd 2784

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  fimacnvinrn  6958  fvcofneq  6978  iunfictbso  9879  axcnre  10929  fseq1p1m1  13339  seqf1olem1  13771  expmulz  13838  expubnd  13904  subsq  13935  bcm1k  14038  bcpasc  14044  cshwcshid  14549  crim  14835  rereb  14840  rlimrecl  15298  iseraltlem2  15403  fsumsplit1  15466  fsumparts  15527  isumshft  15560  geoserg  15587  pwdif  15589  efsub  15818  sincossq  15894  efieq1re  15917  eucalg  16301  lcmfunsnlem  16355  phiprmpw  16486  modprmn0modprm0  16517  coprimeprodsq  16518  pythagtriplem15  16539  pythagtriplem17  16541  fldivp1  16607  1arithlem4  16636  setsidvald  16909  setsidvaldOLD  16910  setsid  16918  pwsbas  17207  invfuc  17701  estrreslem1  17862  latdisdlem  18223  odinv  19177  frgpuplem  19387  gexexlem  19462  fincygsubgodd  19724  srgbinomlem4  19788  gsumdixp  19857  cnfldsub  20635  mplcoe1  21247  evlsvarsrng  21318  ply1idvr1  21473  ply1coe  21476  evls1varsrng  21515  mat1scmat  21697  m1detdiag  21755  mdetunilem7  21776  madugsum  21801  pm2mpmhmlem2  21977  mretopd  22252  upxp  22783  uptx  22785  imasdsf1olem  23535  clmvs2  24266  cphipipcj  24373  cphipval2  24414  itgmulc2lem2  25006  r1pid  25333  coeeulem  25394  fta1lem  25476  aaliou3lem8  25514  eff1olem  25713  tanarg  25783  logcnlem4  25809  root1cj  25918  angpieqvdlem  25987  quad2  25998  dcubic  26005  quart1  26015  jensen  26147  lgamgulmlem5  26191  lgamgulm2  26194  ftalem5  26235  basellem8  26246  chpchtsum  26376  logfaclbnd  26379  perfectlem2  26387  gausslemma2dlem1a  26522  2sqlem3  26577  dchrvmasum2lem  26653  dchrvmasumiflem2  26659  selberglem2  26703  selberg3r  26726  pntlem3  26766  ostth2  26794  ostth3  26795  krippenlem  27060  colinearalglem1  27283  axlowdimlem16  27334  axcontlem4  27344  clwlkclwwlkfo  28382  nmbdoplbi  30395  nmcopexi  30398  nmbdfnlbi  30420  nmcfnexi  30422  nmcfnlbi  30423  hstoh  30603  fcobij  31066  lt2addrd  31083  xlt2addrd  31090  cshwrnid  31242  symgfcoeu  31360  cycpmconjslem2  31431  cycpmconjs  31432  isarchi3  31450  archirngz  31452  dimkerim  31717  submatminr1  31769  mdetpmtr1  31782  madjusmdetlem1  31786  zarcmplem  31840  qqhnm  31949  esumfzf  32046  ddemeas  32213  sseqp1  32371  ballotlemi1  32478  ballotlemii  32479  ballotlemic  32482  ballotlem1c  32483  fsum2dsub  32596  circlemeth  32629  hgt750lemb  32645  hgt750lema  32646  hgt750leme  32647  elmrsubrn  33491  madeoldsuc  34076  cos2h  35777  itg2addnclem  35837  itgmulc2nclem2  35853  areacirclem1  35874  areacirclem4  35877  cntotbnd  35963  atmod2i2  37883  trljat1  38187  trljat2  38188  cdleme9  38274  cdleme15b  38296  cdleme20c  38332  cdleme22eALTN  38366  dvhopN  39137  doca2N  39147  cdlemn10  39227  dochocss  39387  djhlj  39422  dihprrnlem1N  39445  dihprrnlem2  39446  lcfl7lem  39520  lclkrlem2c  39530  hgmapadd  39915  hdmapinvlem3  39941  hgmapvvlem1  39944  nn0expgcd  40342  rmydbl  40769  jm2.18  40817  jm2.19  40822  proot1hash  41032  dssmapnvod  41635  binomcxplemnotnn0  41981  oddfl  42823  dstregt0  42827  supsubc  42899  absimlere  43027  uzinico2  43107  mccllem  43145  ellimcabssub0  43165  sumnnodd  43178  climresmpt  43207  limsupresuz  43251  liminfresuz  43332  coskpi2  43414  cosknegpi  43417  dvsinax  43461  dvnmptdivc  43486  dvnxpaek  43490  dvnmul  43491  dvmptfprodlem  43492  ditgeqiooicc  43508  itgioocnicc  43525  itgspltprt  43527  wallispi2lem2  43620  dirkerper  43644  dirkertrigeqlem2  43647  dirkertrigeqlem3  43648  dirkertrigeq  43649  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem18  43673  fourierdlem19  43674  fourierdlem33  43688  fourierdlem35  43690  fourierdlem41  43696  fourierdlem42  43697  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem53  43707  fourierdlem63  43717  fourierdlem65  43719  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem81  43735  fourierdlem82  43736  fourierdlem83  43737  fourierdlem84  43738  fourierdlem90  43744  fourierdlem93  43747  fourierdlem95  43749  fourierdlem103  43757  fourierdlem104  43758  fourierdlem107  43761  fourierdlem111  43765  fourierswlem  43778  fouriersw  43779  etransclem4  43786  etransclem9  43791  etransclem28  43810  etransclem35  43817  etransclem38  43820  sge0tsms  43925  sge0sup  43936  sge0resplit  43951  sge0split  43954  sge0ss  43957  sge0rpcpnf  43966  sge0isum  43972  sge0xadd  43980  sge0seq  43991  ismeannd  44012  caratheodorylem1  44071  isomenndlem  44075  hoicvrrex  44101  ovn0lem  44110  hoidmvlelem2  44141  hoidmvlelem3  44142  ovnlecvr2  44155  voncmpl  44166  hspmbllem1  44171  hspmbllem2  44172  ovolval4lem1  44194  incsmf  44287  smfpimltmpt  44291  smfpimltxrmptf  44303  decsmf  44312  smfpimgtmpt  44326  smfpimgtxrmptf  44329  smfmullem1  44336  smfinfmpt  44363  smflimsuplem2  44365  sigarac  44379  cevathlem2  44395  fmtnorec3  45011  fmtnorec4  45012  oddflALTV  45126  perfectALTVlem2  45185  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  c0snmgmhm  45483  funcrngcsetc  45567  funcringcsetc  45604  ply1mulgsum  45742  lindslinindsimp2lem5  45814  m1modmmod  45878  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977  nn0sumshdiglem2  45979  itschlc0yqe  46117