Theorem 3eqtrrd 2776

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

Syntax hints:   → wi 4   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  fimacnvinrn  7023  fvcofneq  7045  iunfictbso  10036  axcnre  11087  fseq1p1m1  13552  seqf1olem1  14003  expmulz  14070  expubnd  14140  subsq  14172  bcm1k  14277  bcpasc  14283  cshwcshid  14789  crim  15077  rereb  15082  rlimrecl  15542  iseraltlem2  15645  fsumsplit1  15707  fsumparts  15769  isumshft  15804  geoserg  15831  pwdif  15833  efsub  16067  sincossq  16143  efieq1re  16166  nn0expgcd  16533  eucalg  16556  lcmfunsnlem  16610  phiprmpw  16746  modprmn0modprm0  16778  coprimeprodsq  16779  pythagtriplem15  16800  pythagtriplem17  16802  fldivp1  16868  1arithlem4  16897  setsidvald  17169  setsid  17177  pwsbas  17450  invfuc  17944  estrreslem1  18103  latdisdlem  18462  ghmquskerco  19259  odinv  19536  frgpuplem  19747  gexexlem  19827  fincygsubgodd  20089  srgbinomlem4  20210  gsumdixp  20298  c0snmgmhm  20442  funcrngcsetc  20617  funcringcsetc  20651  cnfldsub  21380  mplcoe1  22015  evlsvarsrng  22085  psdmul  22132  ply1idvr1OLD  22260  ply1coe  22263  evls1varsrng  22305  mat1scmat  22504  m1detdiag  22562  mdetunilem7  22583  madugsum  22608  pm2mpmhmlem2  22784  mretopd  23057  upxp  23588  uptx  23590  imasdsf1olem  24338  clmvs2  25061  cphipipcj  25167  cphipval2  25208  itgmulc2lem2  25800  r1pid  26126  coeeulem  26189  fta1lem  26273  aaliou3lem8  26311  eff1olem  26512  tanarg  26583  logcnlem4  26609  root1cj  26720  angpieqvdlem  26792  quad2  26803  dcubic  26810  quart1  26820  jensen  26952  lgamgulmlem5  26996  lgamgulm2  26999  ftalem5  27040  basellem8  27051  chpchtsum  27182  logfaclbnd  27185  perfectlem2  27193  gausslemma2dlem1a  27328  2sqlem3  27383  dchrvmasum2lem  27459  dchrvmasumiflem2  27465  selberglem2  27509  selberg3r  27532  pntlem3  27572  ostth2  27600  ostth3  27601  madeoldsuc  27877  zseo  28414  addhalfcut  28451  pw2cut2  28454  krippenlem  28758  colinearalglem1  28975  axlowdimlem16  29026  axcontlem4  29036  clwlkclwwlkfo  30079  nmbdoplbi  32095  nmcopexi  32098  nmbdfnlbi  32120  nmcfnexi  32122  nmcfnlbi  32123  hstoh  32303  fcobij  32793  lt2addrd  32823  xlt2addrd  32832  cshwrnid  33021  symgfcoeu  33143  cycpmconjslem2  33216  cycpmconjs  33217  isarchi3  33248  archirngz  33250  elrgspnsubrunlem1  33308  elrspunsn  33489  mxidlirredi  33531  1arithidomlem1  33595  1arithidomlem2  33596  1arithidom  33597  evlextv  33686  esplyfval1  33717  dimkerim  33771  lvecendof1f1o  33777  fldextrspunlsplem  33817  nn0constr  33905  constraddcl  33906  constrnegcl  33907  constrremulcl  33911  constrrecl  33913  constrimcl  33914  constrmulcl  33915  constrreinvcl  33916  constrinvcl  33917  constrresqrtcl  33921  constrabscl  33922  2sqr3minply  33924  submatminr1  33954  mdetpmtr1  33967  madjusmdetlem1  33971  zarcmplem  34025  qqhnm  34134  esumfzf  34213  ddemeas  34380  sseqp1  34539  ballotlemi1  34647  ballotlemii  34648  ballotlemic  34651  ballotlem1c  34652  fsum2dsub  34751  circlemeth  34784  hgt750lemb  34800  hgt750lema  34801  hgt750leme  34802  elmrsubrn  35702  cos2h  37932  itg2addnclem  37992  itgmulc2nclem2  38008  areacirclem1  38029  areacirclem4  38032  cntotbnd  38117  atmod2i2  40308  trljat1  40612  trljat2  40613  cdleme9  40699  cdleme15b  40721  cdleme20c  40757  cdleme22eALTN  40791  dvhopN  41562  doca2N  41572  cdlemn10  41652  dochocss  41812  djhlj  41847  dihprrnlem1N  41870  dihprrnlem2  41871  lcfl7lem  41945  lclkrlem2c  41955  hgmapadd  42340  hdmapinvlem3  42366  hgmapvvlem1  42369  sumcubes  42745  zaddcomlem  42908  fidomncyc  42980  selvvvval  43018  rmydbl  43368  jm2.18  43416  jm2.19  43421  proot1hash  43623  dssmapnvod  44447  binomcxplemnotnn0  44783  oddfl  45711  dstregt0  45715  supsubc  45783  absimlere  45907  uzinico2  45991  mccllem  46027  ellimcabssub0  46047  sumnnodd  46060  climresmpt  46087  limsupresuz  46131  liminfresuz  46212  coskpi2  46294  cosknegpi  46297  dvsinax  46341  dvnmptdivc  46366  dvnxpaek  46370  dvnmul  46371  dvmptfprodlem  46372  ditgeqiooicc  46388  itgioocnicc  46405  itgspltprt  46407  wallispi2lem2  46500  dirkerper  46524  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem18  46553  fourierdlem19  46554  fourierdlem33  46568  fourierdlem35  46570  fourierdlem41  46576  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem53  46587  fourierdlem63  46597  fourierdlem65  46599  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem81  46615  fourierdlem82  46616  fourierdlem83  46617  fourierdlem84  46618  fourierdlem90  46624  fourierdlem93  46627  fourierdlem95  46629  fourierdlem103  46637  fourierdlem104  46638  fourierdlem107  46641  fourierdlem111  46645  fourierswlem  46658  fouriersw  46659  etransclem4  46666  etransclem9  46671  etransclem28  46690  etransclem35  46697  etransclem38  46700  sge0tsms  46808  sge0sup  46819  sge0resplit  46834  sge0split  46837  sge0ss  46840  sge0rpcpnf  46849  sge0isum  46855  sge0xadd  46863  sge0seq  46874  ismeannd  46895  caratheodorylem1  46954  isomenndlem  46958  hoicvrrex  46984  ovn0lem  46993  hoidmvlelem2  47024  hoidmvlelem3  47025  ovnlecvr2  47038  voncmpl  47049  hspmbllem1  47054  hspmbllem2  47055  ovolval4lem1  47077  incsmf  47170  smfpimltmpt  47174  smfpimltxrmptf  47186  decsmf  47195  smfpimgtmpt  47209  smfpimgtxrmptf  47212  smfmullem1  47219  smflimsuplem2  47249  sigarac  47280  cevathlem2  47296  sin3t  47319  cos3t  47320  m1modmmod  47812  fmtnorec3  48011  fmtnorec4  48012  oddflALTV  48139  perfectALTVlem2  48198  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  uspgrlimlem1  48464  gpgvtxedg0  48539  gpgvtxedg1  48540  gpg3kgrtriexlem2  48560  ply1mulgsum  48866  lindslinindsimp2lem5  48938  nn0sumshdiglemA  49095  nn0sumshdiglemB  49096  nn0sumshdiglem2  49098  itschlc0yqe  49236