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  7025  fvcofneq  7047  iunfictbso  10043  axcnre  11093  fseq1p1m1  13535  seqf1olem1  13982  expmulz  14049  expubnd  14119  subsq  14151  bcm1k  14256  bcpasc  14262  cshwcshid  14769  crim  15057  rereb  15062  rlimrecl  15522  iseraltlem2  15625  fsumsplit1  15687  fsumparts  15748  isumshft  15781  geoserg  15808  pwdif  15810  efsub  16044  sincossq  16120  efieq1re  16143  nn0expgcd  16510  eucalg  16533  lcmfunsnlem  16587  phiprmpw  16722  modprmn0modprm0  16754  coprimeprodsq  16755  pythagtriplem15  16776  pythagtriplem17  16778  fldivp1  16844  1arithlem4  16873  setsidvald  17145  setsid  17153  pwsbas  17426  invfuc  17919  estrreslem1  18078  latdisdlem  18437  ghmquskerco  19198  odinv  19475  frgpuplem  19686  gexexlem  19766  fincygsubgodd  20028  srgbinomlem4  20149  gsumdixp  20239  c0snmgmhm  20382  funcrngcsetc  20560  funcringcsetc  20594  cnfldsub  21339  mplcoe1  21977  evlsvarsrng  22039  psdmul  22086  ply1idvr1OLD  22215  ply1coe  22218  evls1varsrng  22260  mat1scmat  22459  m1detdiag  22517  mdetunilem7  22538  madugsum  22563  pm2mpmhmlem2  22739  mretopd  23012  upxp  23543  uptx  23545  imasdsf1olem  24294  clmvs2  25027  cphipipcj  25133  cphipval2  25174  itgmulc2lem2  25767  r1pid  26099  coeeulem  26162  fta1lem  26248  aaliou3lem8  26286  eff1olem  26490  tanarg  26561  logcnlem4  26587  root1cj  26699  angpieqvdlem  26771  quad2  26782  dcubic  26789  quart1  26799  jensen  26932  lgamgulmlem5  26976  lgamgulm2  26979  ftalem5  27020  basellem8  27031  chpchtsum  27163  logfaclbnd  27166  perfectlem2  27174  gausslemma2dlem1a  27309  2sqlem3  27364  dchrvmasum2lem  27440  dchrvmasumiflem2  27446  selberglem2  27490  selberg3r  27513  pntlem3  27553  ostth2  27581  ostth3  27582  madeoldsuc  27834  zseo  28349  addhalfcut  28382  krippenlem  28670  colinearalglem1  28886  axlowdimlem16  28937  axcontlem4  28947  clwlkclwwlkfo  29988  nmbdoplbi  32003  nmcopexi  32006  nmbdfnlbi  32028  nmcfnexi  32030  nmcfnlbi  32031  hstoh  32211  fcobij  32695  lt2addrd  32724  xlt2addrd  32732  cshwrnid  32933  symgfcoeu  33054  cycpmconjslem2  33127  cycpmconjs  33128  isarchi3  33156  archirngz  33158  elrgspnsubrunlem1  33214  elrspunsn  33393  mxidlirredi  33435  1arithidomlem1  33499  1arithidomlem2  33500  1arithidom  33501  dimkerim  33616  lvecendof1f1o  33622  fldextrspunlsplem  33661  nn0constr  33744  constraddcl  33745  constrnegcl  33746  constrremulcl  33750  constrrecl  33752  constrimcl  33753  constrmulcl  33754  constrreinvcl  33755  constrinvcl  33756  constrresqrtcl  33760  constrabscl  33761  2sqr3minply  33763  submatminr1  33793  mdetpmtr1  33806  madjusmdetlem1  33810  zarcmplem  33864  qqhnm  33973  esumfzf  34052  ddemeas  34219  sseqp1  34379  ballotlemi1  34487  ballotlemii  34488  ballotlemic  34491  ballotlem1c  34492  fsum2dsub  34591  circlemeth  34624  hgt750lemb  34640  hgt750lema  34641  hgt750leme  34642  elmrsubrn  35500  cos2h  37598  itg2addnclem  37658  itgmulc2nclem2  37674  areacirclem1  37695  areacirclem4  37698  cntotbnd  37783  atmod2i2  39849  trljat1  40153  trljat2  40154  cdleme9  40240  cdleme15b  40262  cdleme20c  40298  cdleme22eALTN  40332  dvhopN  41103  doca2N  41113  cdlemn10  41193  dochocss  41353  djhlj  41388  dihprrnlem1N  41411  dihprrnlem2  41412  lcfl7lem  41486  lclkrlem2c  41496  hgmapadd  41881  hdmapinvlem3  41907  hgmapvvlem1  41910  sumcubes  42294  zaddcomlem  42444  fidomncyc  42516  selvvvval  42566  rmydbl  42922  jm2.18  42970  jm2.19  42975  proot1hash  43177  dssmapnvod  44002  binomcxplemnotnn0  44338  oddfl  45269  dstregt0  45273  supsubc  45342  absimlere  45468  uzinico2  45552  mccllem  45588  ellimcabssub0  45608  sumnnodd  45621  climresmpt  45650  limsupresuz  45694  liminfresuz  45775  coskpi2  45857  cosknegpi  45860  dvsinax  45904  dvnmptdivc  45929  dvnxpaek  45933  dvnmul  45934  dvmptfprodlem  45935  ditgeqiooicc  45951  itgioocnicc  45968  itgspltprt  45970  wallispi2lem2  46063  dirkerper  46087  dirkertrigeqlem2  46090  dirkertrigeqlem3  46091  dirkertrigeq  46092  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem18  46116  fourierdlem19  46117  fourierdlem33  46131  fourierdlem35  46133  fourierdlem41  46139  fourierdlem42  46140  fourierdlem48  46145  fourierdlem49  46146  fourierdlem50  46147  fourierdlem53  46150  fourierdlem63  46160  fourierdlem65  46162  fourierdlem73  46170  fourierdlem74  46171  fourierdlem75  46172  fourierdlem81  46178  fourierdlem82  46179  fourierdlem83  46180  fourierdlem84  46181  fourierdlem90  46187  fourierdlem93  46190  fourierdlem95  46192  fourierdlem103  46200  fourierdlem104  46201  fourierdlem107  46204  fourierdlem111  46208  fourierswlem  46221  fouriersw  46222  etransclem4  46229  etransclem9  46234  etransclem28  46253  etransclem35  46260  etransclem38  46263  sge0tsms  46371  sge0sup  46382  sge0resplit  46397  sge0split  46400  sge0ss  46403  sge0rpcpnf  46412  sge0isum  46418  sge0xadd  46426  sge0seq  46437  ismeannd  46458  caratheodorylem1  46517  isomenndlem  46521  hoicvrrex  46547  ovn0lem  46556  hoidmvlelem2  46587  hoidmvlelem3  46588  ovnlecvr2  46601  voncmpl  46612  hspmbllem1  46617  hspmbllem2  46618  ovolval4lem1  46640  incsmf  46733  smfpimltmpt  46737  smfpimltxrmptf  46749  decsmf  46758  smfpimgtmpt  46772  smfpimgtxrmptf  46775  smfmullem1  46782  smflimsuplem2  46812  sigarac  46843  cevathlem2  46859  m1modmmod  47352  fmtnorec3  47542  fmtnorec4  47543  oddflALTV  47657  perfectALTVlem2  47716  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  uspgrlimlem1  47980  gpgvtxedg0  48047  gpgvtxedg1  48048  gpg3kgrtriexlem2  48068  ply1mulgsum  48372  lindslinindsimp2lem5  48444  nn0sumshdiglemA  48601  nn0sumshdiglemB  48602  nn0sumshdiglem2  48604  itschlc0yqe  48742