Theorem 3eqtrrd 2800

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752

This theorem is used by:  fimacnvinrn  7065  fvcofneq  7087  iunfictbso  10120  axcnre  11176  fseq1p1m1  13656  seqf1olem1  14108  expmulz  14175  expubnd  14245  subsq  14277  bcm1k  14382  bcpasc  14388  cshwcshid  14901  crim  15205  rereb  15210  rlimrecl  15670  iseraltlem2  15773  fsumsplit1  15834  fsumparts  15896  isumshft  15931  geoserg  15958  pwdif  15960  efsub  16191  sincossq  16267  efieq1re  16290  nn0expgcd  16657  eucalg  16680  lcmfunsnlem  16734  phiprmpw  16870  modprmn0modprm0  16902  coprimeprodsq  16903  pythagtriplem15  16924  pythagtriplem17  16926  fldivp1  16992  1arithlem4  17021  setsidvald  17294  setsid  17302  pwsbas  17575  invfuc  18069  estrreslem1  18228  latdisdlem  18587  ghmquskerco  19414  odinv  19691  frgpuplem  19902  gexexlem  19982  fincygsubgodd  20244  srgbinomlem4  20371  gsumdixp  20462  c0snmgmhm  20606  funcrngcsetc  20805  funcringcsetc  20839  cnfldsub  21616  mplcoe1  22256  evlsvarsrng  22326  selvvvval  22361  psdmul  22397  ply1coe  22526  evls1varsrng  22568  mat1scmat  22764  m1detdiag  22822  mdetunilem7  22843  madugsum  22868  pm2mpmhmlem2  23047  mretopd  23320  upxp  23852  uptx  23854  imasdsf1olem  24602  clmvs2  25325  cphipipcj  25431  cphipval2  25472  itgmulc2lem2  26063  r1pid  26389  coeeulem  26453  fta1lem  26540  aaliou3lem8  26584  eff1olem  26788  tanarg  26859  logcnlem4  26885  root1cj  26996  angpieqvdlem  27068  quad2  27079  dcubic  27086  quart1  27096  jensen  27228  lgamgulmlem5  27272  lgamgulm2  27275  ftalem5  27316  basellem8  27327  chpchtsum  27458  logfaclbnd  27461  perfectlem2  27469  gausslemma2dlem1a  27604  2sqlem3  27659  dchrvmasum2lem  27735  dchrvmasumiflem2  27741  selberglem2  27785  selberg3r  27808  pntlem3  27848  ostth2  27876  ostth3  27877  madeoldsuc  28153  zseo  28690  addhalfcut  28727  pw2cut2  28730  krippenlem  29044  colinearalglem1  29366  axlowdimlem16  29417  axcontlem4  29427  clwlkclwwlkfo  30482  nmbdoplbi  32508  nmcopexi  32511  nmbdfnlbi  32533  nmcfnexi  32535  nmcfnlbi  32536  hstoh  32716  fcobij  33194  lt2addrd  33224  xlt2addrd  33233  cshwrnid  33404  symgfcoeu  33525  cycpmconjslem2  33598  cycpmconjs  33599  isarchi3  33630  archirngz  33632  elrgspnsubrunlem1  33690  elrspunsn  33860  mxidlirredi  33877  1arithidomlem1  33948  1arithidomlem2  33949  1arithidom  33950  evlextv  34055  esplyfval1  34086  dimkerim  34140  lvecendof1f1o  34146  fldextrspunlsplem  34186  nn0constr  34274  constraddcl  34275  constrnegcl  34276  constrremulcl  34280  constrrecl  34282  constrimcl  34283  constrmulcl  34284  constrreinvcl  34285  constrinvcl  34286  constrresqrtcl  34290  constrabscl  34291  2sqr3minply  34293  submatminr1  34323  mdetpmtr1  34336  madjusmdetlem1  34340  zarcmplem  34394  qqhnm  34503  esumfzf  34582  ddemeas  34750  sseqp1  34909  ballotlemi1  35017  ballotlemii  35018  ballotlemic  35021  ballotlem1c  35022  fsum2dsub  35118  circlemeth  35151  hgt750lemb  35167  hgt750lema  35168  hgt750leme  35169  elmrsubrn  36102  nadddilem1  36803  cos2h  38368  itg2addnclem  38423  itgmulc2nclem2  38439  areacirclem1  38460  areacirclem4  38463  cntotbnd  38549  atmod2i2  40738  trljat1  41042  trljat2  41043  cdleme9  41129  cdleme15b  41151  cdleme20c  41187  cdleme22eALTN  41221  dvhopN  41992  doca2N  42002  cdlemn10  42082  dochocss  42242  djhlj  42277  dihprrnlem1N  42300  dihprrnlem2  42301  lcfl7lem  42375  lclkrlem2c  42385  hgmapadd  42770  hdmapinvlem3  42796  hgmapvvlem1  42799  sumcubes  43191  zaddcomlem  43354  fidomncyc  43420  rmydbl  43784  jm2.18  43832  jm2.19  43837  proot1hash  44039  dssmapnvod  44863  binomcxplemnotnn0  45183  oddfl  46114  dstregt0  46118  supsubc  46186  absimlere  46310  uzinico2  46394  mccllem  46430  ellimcabssub0  46450  sumnnodd  46463  climresmpt  46490  limsupresuz  46534  liminfresuz  46615  coskpi2  46697  cosknegpi  46700  dvsinax  46744  dvnmptdivc  46769  dvnxpaek  46773  dvnmul  46774  dvmptfprodlem  46775  ditgeqiooicc  46791  itgioocnicc  46808  itgspltprt  46810  wallispi2lem2  46903  dirkerper  46927  dirkertrigeqlem2  46930  dirkertrigeqlem3  46931  dirkertrigeq  46932  dirkercncflem2  46935  dirkercncflem4  46937  fourierdlem18  46956  fourierdlem19  46957  fourierdlem33  46971  fourierdlem35  46973  fourierdlem41  46979  fourierdlem42  46980  fourierdlem48  46985  fourierdlem49  46986  fourierdlem50  46987  fourierdlem53  46990  fourierdlem63  47000  fourierdlem65  47002  fourierdlem73  47010  fourierdlem74  47011  fourierdlem75  47012  fourierdlem81  47018  fourierdlem82  47019  fourierdlem83  47020  fourierdlem84  47021  fourierdlem90  47027  fourierdlem93  47030  fourierdlem95  47032  fourierdlem103  47040  fourierdlem104  47041  fourierdlem107  47044  fourierdlem111  47048  fourierswlem  47061  fouriersw  47062  etransclem4  47069  etransclem9  47074  etransclem28  47093  etransclem35  47100  etransclem38  47103  sge0tsms  47211  sge0sup  47222  sge0resplit  47237  sge0split  47240  sge0ss  47243  sge0rpcpnf  47252  sge0isum  47258  sge0xadd  47266  sge0seq  47277  ismeannd  47298  caratheodorylem1  47357  isomenndlem  47361  hoicvrrex  47387  ovn0lem  47396  hoidmvlelem2  47427  hoidmvlelem3  47428  ovnlecvr2  47441  voncmpl  47452  hspmbllem1  47457  hspmbllem2  47458  ovolval4lem1  47480  incsmf  47573  smfpimltmpt  47577  smfpimltxrmptf  47589  decsmf  47598  smfpimgtmpt  47612  smfpimgtxrmptf  47615  smfmullem1  47622  smflimsuplem2  47652  sigarac  47683  cevathlem2  47699  sin3t  47738  cos3t  47739  m1modmmod  48255  fmtnorec3  48454  fmtnorec4  48455  oddflALTV  48582  perfectALTVlem2  48641  nnsum4primeseven  48719  nnsum4primesevenALTV  48720  uspgrlimlem1  48907  gpgvtxedg0  48982  gpgvtxedg1  48983  gpg3kgrtriexlem2  49003  ply1mulgsum  49323  lindslinindsimp2lem5  49395  nn0sumshdiglemA  49552  nn0sumshdiglemB  49553  nn0sumshdiglem2  49555  itschlc0yqe  49693