Theorem 3eqtrrd 2769

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  fimacnvinrn  7043  fvcofneq  7065  iunfictbso  10067  axcnre  11117  fseq1p1m1  13559  seqf1olem1  14006  expmulz  14073  expubnd  14143  subsq  14175  bcm1k  14280  bcpasc  14286  cshwcshid  14793  crim  15081  rereb  15086  rlimrecl  15546  iseraltlem2  15649  fsumsplit1  15711  fsumparts  15772  isumshft  15805  geoserg  15832  pwdif  15834  efsub  16068  sincossq  16144  efieq1re  16167  nn0expgcd  16534  eucalg  16557  lcmfunsnlem  16611  phiprmpw  16746  modprmn0modprm0  16778  coprimeprodsq  16779  pythagtriplem15  16800  pythagtriplem17  16802  fldivp1  16868  1arithlem4  16897  setsidvald  17169  setsid  17177  pwsbas  17450  invfuc  17939  estrreslem1  18098  latdisdlem  18455  ghmquskerco  19216  odinv  19491  frgpuplem  19702  gexexlem  19782  fincygsubgodd  20044  srgbinomlem4  20138  gsumdixp  20228  c0snmgmhm  20371  funcrngcsetc  20549  funcringcsetc  20583  cnfldsub  21309  mplcoe1  21944  evlsvarsrng  22006  psdmul  22053  ply1idvr1OLD  22182  ply1coe  22185  evls1varsrng  22227  mat1scmat  22426  m1detdiag  22484  mdetunilem7  22505  madugsum  22530  pm2mpmhmlem2  22706  mretopd  22979  upxp  23510  uptx  23512  imasdsf1olem  24261  clmvs2  24994  cphipipcj  25100  cphipval2  25141  itgmulc2lem2  25734  r1pid  26066  coeeulem  26129  fta1lem  26215  aaliou3lem8  26253  eff1olem  26457  tanarg  26528  logcnlem4  26554  root1cj  26666  angpieqvdlem  26738  quad2  26749  dcubic  26756  quart1  26766  jensen  26899  lgamgulmlem5  26943  lgamgulm2  26946  ftalem5  26987  basellem8  26998  chpchtsum  27130  logfaclbnd  27133  perfectlem2  27141  gausslemma2dlem1a  27276  2sqlem3  27331  dchrvmasum2lem  27407  dchrvmasumiflem2  27413  selberglem2  27457  selberg3r  27480  pntlem3  27520  ostth2  27548  ostth3  27549  madeoldsuc  27796  zseo  28308  addhalfcut  28334  krippenlem  28617  colinearalglem1  28833  axlowdimlem16  28884  axcontlem4  28894  clwlkclwwlkfo  29938  nmbdoplbi  31953  nmcopexi  31956  nmbdfnlbi  31978  nmcfnexi  31980  nmcfnlbi  31981  hstoh  32161  fcobij  32645  lt2addrd  32674  xlt2addrd  32682  cshwrnid  32883  symgfcoeu  33039  cycpmconjslem2  33112  cycpmconjs  33113  isarchi3  33141  archirngz  33143  elrgspnsubrunlem1  33198  elrspunsn  33400  mxidlirredi  33442  1arithidomlem1  33506  1arithidomlem2  33507  1arithidom  33508  dimkerim  33623  lvecendof1f1o  33629  fldextrspunlsplem  33668  nn0constr  33751  constraddcl  33752  constrnegcl  33753  constrremulcl  33757  constrrecl  33759  constrimcl  33760  constrmulcl  33761  constrreinvcl  33762  constrinvcl  33763  constrresqrtcl  33767  constrabscl  33768  2sqr3minply  33770  submatminr1  33800  mdetpmtr1  33813  madjusmdetlem1  33817  zarcmplem  33871  qqhnm  33980  esumfzf  34059  ddemeas  34226  sseqp1  34386  ballotlemi1  34494  ballotlemii  34495  ballotlemic  34498  ballotlem1c  34499  fsum2dsub  34598  circlemeth  34631  hgt750lemb  34647  hgt750lema  34648  hgt750leme  34649  elmrsubrn  35507  cos2h  37605  itg2addnclem  37665  itgmulc2nclem2  37681  areacirclem1  37702  areacirclem4  37705  cntotbnd  37790  atmod2i2  39856  trljat1  40160  trljat2  40161  cdleme9  40247  cdleme15b  40269  cdleme20c  40305  cdleme22eALTN  40339  dvhopN  41110  doca2N  41120  cdlemn10  41200  dochocss  41360  djhlj  41395  dihprrnlem1N  41418  dihprrnlem2  41419  lcfl7lem  41493  lclkrlem2c  41503  hgmapadd  41888  hdmapinvlem3  41914  hgmapvvlem1  41917  sumcubes  42301  zaddcomlem  42451  fidomncyc  42523  selvvvval  42573  rmydbl  42929  jm2.18  42977  jm2.19  42982  proot1hash  43184  dssmapnvod  44009  binomcxplemnotnn0  44345  oddfl  45276  dstregt0  45280  supsubc  45349  absimlere  45475  uzinico2  45559  mccllem  45595  ellimcabssub0  45615  sumnnodd  45628  climresmpt  45657  limsupresuz  45701  liminfresuz  45782  coskpi2  45864  cosknegpi  45867  dvsinax  45911  dvnmptdivc  45936  dvnxpaek  45940  dvnmul  45941  dvmptfprodlem  45942  ditgeqiooicc  45958  itgioocnicc  45975  itgspltprt  45977  wallispi2lem2  46070  dirkerper  46094  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem18  46123  fourierdlem19  46124  fourierdlem33  46138  fourierdlem35  46140  fourierdlem41  46146  fourierdlem42  46147  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem53  46157  fourierdlem63  46167  fourierdlem65  46169  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem81  46185  fourierdlem82  46186  fourierdlem83  46187  fourierdlem84  46188  fourierdlem90  46194  fourierdlem93  46197  fourierdlem95  46199  fourierdlem103  46207  fourierdlem104  46208  fourierdlem107  46211  fourierdlem111  46215  fourierswlem  46228  fouriersw  46229  etransclem4  46236  etransclem9  46241  etransclem28  46260  etransclem35  46267  etransclem38  46270  sge0tsms  46378  sge0sup  46389  sge0resplit  46404  sge0split  46407  sge0ss  46410  sge0rpcpnf  46419  sge0isum  46425  sge0xadd  46433  sge0seq  46444  ismeannd  46465  caratheodorylem1  46524  isomenndlem  46528  hoicvrrex  46554  ovn0lem  46563  hoidmvlelem2  46594  hoidmvlelem3  46595  ovnlecvr2  46608  voncmpl  46619  hspmbllem1  46624  hspmbllem2  46625  ovolval4lem1  46647  incsmf  46740  smfpimltmpt  46744  smfpimltxrmptf  46756  decsmf  46765  smfpimgtmpt  46779  smfpimgtxrmptf  46782  smfmullem1  46789  smflimsuplem2  46819  sigarac  46850  cevathlem2  46866  m1modmmod  47359  fmtnorec3  47549  fmtnorec4  47550  oddflALTV  47664  perfectALTVlem2  47723  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  uspgrlimlem1  47987  gpgvtxedg0  48054  gpgvtxedg1  48055  gpg3kgrtriexlem2  48075  ply1mulgsum  48379  lindslinindsimp2lem5  48451  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  nn0sumshdiglem2  48611  itschlc0yqe  48749