Theorem 3eqtrrd 2774

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 2769	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtrd.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2770	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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

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

This theorem is referenced by:  fimacnvinrn  7014  fvcofneq  7036  iunfictbso  10022  axcnre  11073  fseq1p1m1  13512  seqf1olem1  13962  expmulz  14029  expubnd  14099  subsq  14131  bcm1k  14236  bcpasc  14242  cshwcshid  14748  crim  15036  rereb  15041  rlimrecl  15501  iseraltlem2  15604  fsumsplit1  15666  fsumparts  15727  isumshft  15760  geoserg  15787  pwdif  15789  efsub  16023  sincossq  16099  efieq1re  16122  nn0expgcd  16489  eucalg  16512  lcmfunsnlem  16566  phiprmpw  16701  modprmn0modprm0  16733  coprimeprodsq  16734  pythagtriplem15  16755  pythagtriplem17  16757  fldivp1  16823  1arithlem4  16852  setsidvald  17124  setsid  17132  pwsbas  17405  invfuc  17899  estrreslem1  18058  latdisdlem  18417  ghmquskerco  19211  odinv  19488  frgpuplem  19699  gexexlem  19779  fincygsubgodd  20041  srgbinomlem4  20162  gsumdixp  20252  c0snmgmhm  20396  funcrngcsetc  20571  funcringcsetc  20605  cnfldsub  21350  mplcoe1  21990  evlsvarsrng  22060  psdmul  22107  ply1idvr1OLD  22237  ply1coe  22240  evls1varsrng  22282  mat1scmat  22481  m1detdiag  22539  mdetunilem7  22560  madugsum  22585  pm2mpmhmlem2  22761  mretopd  23034  upxp  23565  uptx  23567  imasdsf1olem  24315  clmvs2  25048  cphipipcj  25154  cphipval2  25195  itgmulc2lem2  25788  r1pid  26120  coeeulem  26183  fta1lem  26269  aaliou3lem8  26307  eff1olem  26511  tanarg  26582  logcnlem4  26608  root1cj  26720  angpieqvdlem  26792  quad2  26803  dcubic  26810  quart1  26820  jensen  26953  lgamgulmlem5  26997  lgamgulm2  27000  ftalem5  27041  basellem8  27052  chpchtsum  27184  logfaclbnd  27187  perfectlem2  27195  gausslemma2dlem1a  27330  2sqlem3  27385  dchrvmasum2lem  27461  dchrvmasumiflem2  27467  selberglem2  27511  selberg3r  27534  pntlem3  27574  ostth2  27602  ostth3  27603  madeoldsuc  27857  zseo  28380  addhalfcut  28416  pw2cut2  28419  krippenlem  28711  colinearalglem1  28928  axlowdimlem16  28979  axcontlem4  28989  clwlkclwwlkfo  30033  nmbdoplbi  32048  nmcopexi  32051  nmbdfnlbi  32073  nmcfnexi  32075  nmcfnlbi  32076  hstoh  32256  fcobij  32748  lt2addrd  32779  xlt2addrd  32788  cshwrnid  32992  symgfcoeu  33113  cycpmconjslem2  33186  cycpmconjs  33187  isarchi3  33218  archirngz  33220  elrgspnsubrunlem1  33278  elrspunsn  33459  mxidlirredi  33501  1arithidomlem1  33565  1arithidomlem2  33566  1arithidom  33567  evlextv  33656  dimkerim  33733  lvecendof1f1o  33739  fldextrspunlsplem  33779  nn0constr  33867  constraddcl  33868  constrnegcl  33869  constrremulcl  33873  constrrecl  33875  constrimcl  33876  constrmulcl  33877  constrreinvcl  33878  constrinvcl  33879  constrresqrtcl  33883  constrabscl  33884  2sqr3minply  33886  submatminr1  33916  mdetpmtr1  33929  madjusmdetlem1  33933  zarcmplem  33987  qqhnm  34096  esumfzf  34175  ddemeas  34342  sseqp1  34501  ballotlemi1  34609  ballotlemii  34610  ballotlemic  34613  ballotlem1c  34614  fsum2dsub  34713  circlemeth  34746  hgt750lemb  34762  hgt750lema  34763  hgt750leme  34764  elmrsubrn  35663  cos2h  37751  itg2addnclem  37811  itgmulc2nclem2  37827  areacirclem1  37848  areacirclem4  37851  cntotbnd  37936  atmod2i2  40061  trljat1  40365  trljat2  40366  cdleme9  40452  cdleme15b  40474  cdleme20c  40510  cdleme22eALTN  40544  dvhopN  41315  doca2N  41325  cdlemn10  41405  dochocss  41565  djhlj  41600  dihprrnlem1N  41623  dihprrnlem2  41624  lcfl7lem  41698  lclkrlem2c  41708  hgmapadd  42093  hdmapinvlem3  42119  hgmapvvlem1  42122  sumcubes  42510  zaddcomlem  42660  fidomncyc  42732  selvvvval  42770  rmydbl  43124  jm2.18  43172  jm2.19  43177  proot1hash  43379  dssmapnvod  44203  binomcxplemnotnn0  44539  oddfl  45468  dstregt0  45472  supsubc  45540  absimlere  45665  uzinico2  45749  mccllem  45785  ellimcabssub0  45805  sumnnodd  45818  climresmpt  45845  limsupresuz  45889  liminfresuz  45970  coskpi2  46052  cosknegpi  46055  dvsinax  46099  dvnmptdivc  46124  dvnxpaek  46128  dvnmul  46129  dvmptfprodlem  46130  ditgeqiooicc  46146  itgioocnicc  46163  itgspltprt  46165  wallispi2lem2  46258  dirkerper  46282  dirkertrigeqlem2  46285  dirkertrigeqlem3  46286  dirkertrigeq  46287  dirkercncflem2  46290  dirkercncflem4  46292  fourierdlem18  46311  fourierdlem19  46312  fourierdlem33  46326  fourierdlem35  46328  fourierdlem41  46334  fourierdlem42  46335  fourierdlem48  46340  fourierdlem49  46341  fourierdlem50  46342  fourierdlem53  46345  fourierdlem63  46355  fourierdlem65  46357  fourierdlem73  46365  fourierdlem74  46366  fourierdlem75  46367  fourierdlem81  46373  fourierdlem82  46374  fourierdlem83  46375  fourierdlem84  46376  fourierdlem90  46382  fourierdlem93  46385  fourierdlem95  46387  fourierdlem103  46395  fourierdlem104  46396  fourierdlem107  46399  fourierdlem111  46403  fourierswlem  46416  fouriersw  46417  etransclem4  46424  etransclem9  46429  etransclem28  46448  etransclem35  46455  etransclem38  46458  sge0tsms  46566  sge0sup  46577  sge0resplit  46592  sge0split  46595  sge0ss  46598  sge0rpcpnf  46607  sge0isum  46613  sge0xadd  46621  sge0seq  46632  ismeannd  46653  caratheodorylem1  46712  isomenndlem  46716  hoicvrrex  46742  ovn0lem  46751  hoidmvlelem2  46782  hoidmvlelem3  46783  ovnlecvr2  46796  voncmpl  46807  hspmbllem1  46812  hspmbllem2  46813  ovolval4lem1  46835  incsmf  46928  smfpimltmpt  46932  smfpimltxrmptf  46944  decsmf  46953  smfpimgtmpt  46967  smfpimgtxrmptf  46970  smfmullem1  46977  smflimsuplem2  47007  sigarac  47038  cevathlem2  47054  m1modmmod  47546  fmtnorec3  47736  fmtnorec4  47737  oddflALTV  47851  perfectALTVlem2  47910  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  uspgrlimlem1  48176  gpgvtxedg0  48251  gpgvtxedg1  48252  gpg3kgrtriexlem2  48272  ply1mulgsum  48578  lindslinindsimp2lem5  48650  nn0sumshdiglemA  48807  nn0sumshdiglemB  48808  nn0sumshdiglem2  48810  itschlc0yqe  48948