Theorem 3eqtrrd 2785

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  fimacnvinrn  7105  fvcofneq  7127  iunfictbso  10183  axcnre  11233  fseq1p1m1  13658  seqf1olem1  14092  expmulz  14159  expubnd  14227  subsq  14259  bcm1k  14364  bcpasc  14370  cshwcshid  14876  crim  15164  rereb  15169  rlimrecl  15626  iseraltlem2  15731  fsumsplit1  15793  fsumparts  15854  isumshft  15887  geoserg  15914  pwdif  15916  efsub  16148  sincossq  16224  efieq1re  16247  nn0expgcd  16611  eucalg  16634  lcmfunsnlem  16688  phiprmpw  16823  modprmn0modprm0  16854  coprimeprodsq  16855  pythagtriplem15  16876  pythagtriplem17  16878  fldivp1  16944  1arithlem4  16973  setsidvald  17246  setsidvaldOLD  17247  setsid  17255  pwsbas  17547  invfuc  18044  estrreslem1  18205  latdisdlem  18566  ghmquskerco  19324  odinv  19603  frgpuplem  19814  gexexlem  19894  fincygsubgodd  20156  srgbinomlem4  20256  gsumdixp  20342  c0snmgmhm  20488  funcrngcsetc  20662  funcringcsetc  20696  cnfldsub  21433  mplcoe1  22078  evlsvarsrng  22146  psdmul  22193  ply1idvr1OLD  22320  ply1coe  22323  evls1varsrng  22365  mat1scmat  22566  m1detdiag  22624  mdetunilem7  22645  madugsum  22670  pm2mpmhmlem2  22846  mretopd  23121  upxp  23652  uptx  23654  imasdsf1olem  24404  clmvs2  25146  cphipipcj  25253  cphipval2  25294  itgmulc2lem2  25888  r1pid  26220  coeeulem  26283  fta1lem  26367  aaliou3lem8  26405  eff1olem  26608  tanarg  26679  logcnlem4  26705  root1cj  26817  angpieqvdlem  26889  quad2  26900  dcubic  26907  quart1  26917  jensen  27050  lgamgulmlem5  27094  lgamgulm2  27097  ftalem5  27138  basellem8  27149  chpchtsum  27281  logfaclbnd  27284  perfectlem2  27292  gausslemma2dlem1a  27427  2sqlem3  27482  dchrvmasum2lem  27558  dchrvmasumiflem2  27564  selberglem2  27608  selberg3r  27631  pntlem3  27671  ostth2  27699  ostth3  27700  madeoldsuc  27941  zseo  28424  addhalfcut  28437  krippenlem  28716  colinearalglem1  28939  axlowdimlem16  28990  axcontlem4  29000  clwlkclwwlkfo  30041  nmbdoplbi  32056  nmcopexi  32059  nmbdfnlbi  32081  nmcfnexi  32083  nmcfnlbi  32084  hstoh  32264  fcobij  32736  lt2addrd  32758  xlt2addrd  32765  cshwrnid  32928  symgfcoeu  33075  cycpmconjslem2  33148  cycpmconjs  33149  isarchi3  33167  archirngz  33169  elrspunsn  33422  mxidlirredi  33464  1arithidomlem1  33528  1arithidomlem2  33529  1arithidom  33530  dimkerim  33640  lvecendof1f1o  33646  2sqr3minply  33738  submatminr1  33756  mdetpmtr1  33769  madjusmdetlem1  33773  zarcmplem  33827  qqhnm  33936  esumfzf  34033  ddemeas  34200  sseqp1  34360  ballotlemi1  34467  ballotlemii  34468  ballotlemic  34471  ballotlem1c  34472  fsum2dsub  34584  circlemeth  34617  hgt750lemb  34633  hgt750lema  34634  hgt750leme  34635  elmrsubrn  35488  cos2h  37571  itg2addnclem  37631  itgmulc2nclem2  37647  areacirclem1  37668  areacirclem4  37671  cntotbnd  37756  atmod2i2  39819  trljat1  40123  trljat2  40124  cdleme9  40210  cdleme15b  40232  cdleme20c  40268  cdleme22eALTN  40302  dvhopN  41073  doca2N  41083  cdlemn10  41163  dochocss  41323  djhlj  41358  dihprrnlem1N  41381  dihprrnlem2  41382  lcfl7lem  41456  lclkrlem2c  41466  hgmapadd  41851  hdmapinvlem3  41877  hgmapvvlem1  41880  sumcubes  42301  zaddcomlem  42427  fidomncyc  42490  selvvvval  42540  rmydbl  42897  jm2.18  42945  jm2.19  42950  proot1hash  43156  dssmapnvod  43982  binomcxplemnotnn0  44325  oddfl  45192  dstregt0  45196  supsubc  45268  absimlere  45395  uzinico2  45480  mccllem  45518  ellimcabssub0  45538  sumnnodd  45551  climresmpt  45580  limsupresuz  45624  liminfresuz  45705  coskpi2  45787  cosknegpi  45790  dvsinax  45834  dvnmptdivc  45859  dvnxpaek  45863  dvnmul  45864  dvmptfprodlem  45865  ditgeqiooicc  45881  itgioocnicc  45898  itgspltprt  45900  wallispi2lem2  45993  dirkerper  46017  dirkertrigeqlem2  46020  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem18  46046  fourierdlem19  46047  fourierdlem33  46061  fourierdlem35  46063  fourierdlem41  46069  fourierdlem42  46070  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem53  46080  fourierdlem63  46090  fourierdlem65  46092  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem81  46108  fourierdlem82  46109  fourierdlem83  46110  fourierdlem84  46111  fourierdlem90  46117  fourierdlem93  46120  fourierdlem95  46122  fourierdlem103  46130  fourierdlem104  46131  fourierdlem107  46134  fourierdlem111  46138  fourierswlem  46151  fouriersw  46152  etransclem4  46159  etransclem9  46164  etransclem28  46183  etransclem35  46190  etransclem38  46193  sge0tsms  46301  sge0sup  46312  sge0resplit  46327  sge0split  46330  sge0ss  46333  sge0rpcpnf  46342  sge0isum  46348  sge0xadd  46356  sge0seq  46367  ismeannd  46388  caratheodorylem1  46447  isomenndlem  46451  hoicvrrex  46477  ovn0lem  46486  hoidmvlelem2  46517  hoidmvlelem3  46518  ovnlecvr2  46531  voncmpl  46542  hspmbllem1  46547  hspmbllem2  46548  ovolval4lem1  46570  incsmf  46663  smfpimltmpt  46667  smfpimltxrmptf  46679  decsmf  46688  smfpimgtmpt  46702  smfpimgtxrmptf  46705  smfmullem1  46712  smfinfmpt  46740  smflimsuplem2  46742  sigarac  46773  cevathlem2  46789  fmtnorec3  47422  fmtnorec4  47423  oddflALTV  47537  perfectALTVlem2  47596  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  uspgrlimlem1  47812  ply1mulgsum  48119  lindslinindsimp2lem5  48191  m1modmmod  48255  nn0sumshdiglemA  48353  nn0sumshdiglemB  48354  nn0sumshdiglem2  48356  itschlc0yqe  48494