Theorem 3eqtrrd 2773

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

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

This theorem is referenced by:  fimacnvinrn  7010  fvcofneq  7032  iunfictbso  10012  axcnre  11062  fseq1p1m1  13500  seqf1olem1  13950  expmulz  14017  expubnd  14087  subsq  14119  bcm1k  14224  bcpasc  14230  cshwcshid  14736  crim  15024  rereb  15029  rlimrecl  15489  iseraltlem2  15592  fsumsplit1  15654  fsumparts  15715  isumshft  15748  geoserg  15775  pwdif  15777  efsub  16011  sincossq  16087  efieq1re  16110  nn0expgcd  16477  eucalg  16500  lcmfunsnlem  16554  phiprmpw  16689  modprmn0modprm0  16721  coprimeprodsq  16722  pythagtriplem15  16743  pythagtriplem17  16745  fldivp1  16811  1arithlem4  16840  setsidvald  17112  setsid  17120  pwsbas  17393  invfuc  17886  estrreslem1  18045  latdisdlem  18404  ghmquskerco  19198  odinv  19475  frgpuplem  19686  gexexlem  19766  fincygsubgodd  20028  srgbinomlem4  20149  gsumdixp  20239  c0snmgmhm  20382  funcrngcsetc  20557  funcringcsetc  20591  cnfldsub  21336  mplcoe1  21973  evlsvarsrng  22035  psdmul  22082  ply1idvr1OLD  22211  ply1coe  22214  evls1varsrng  22256  mat1scmat  22455  m1detdiag  22513  mdetunilem7  22534  madugsum  22559  pm2mpmhmlem2  22735  mretopd  23008  upxp  23539  uptx  23541  imasdsf1olem  24289  clmvs2  25022  cphipipcj  25128  cphipval2  25169  itgmulc2lem2  25762  r1pid  26094  coeeulem  26157  fta1lem  26243  aaliou3lem8  26281  eff1olem  26485  tanarg  26556  logcnlem4  26582  root1cj  26694  angpieqvdlem  26766  quad2  26777  dcubic  26784  quart1  26794  jensen  26927  lgamgulmlem5  26971  lgamgulm2  26974  ftalem5  27015  basellem8  27026  chpchtsum  27158  logfaclbnd  27161  perfectlem2  27169  gausslemma2dlem1a  27304  2sqlem3  27359  dchrvmasum2lem  27435  dchrvmasumiflem2  27441  selberglem2  27485  selberg3r  27508  pntlem3  27548  ostth2  27576  ostth3  27577  madeoldsuc  27831  zseo  28346  addhalfcut  28380  pw2cut2  28383  krippenlem  28669  colinearalglem1  28886  axlowdimlem16  28937  axcontlem4  28947  clwlkclwwlkfo  29991  nmbdoplbi  32006  nmcopexi  32009  nmbdfnlbi  32031  nmcfnexi  32033  nmcfnlbi  32034  hstoh  32214  fcobij  32707  lt2addrd  32738  xlt2addrd  32746  cshwrnid  32949  symgfcoeu  33058  cycpmconjslem2  33131  cycpmconjs  33132  isarchi3  33163  archirngz  33165  elrgspnsubrunlem1  33221  elrspunsn  33401  mxidlirredi  33443  1arithidomlem1  33507  1arithidomlem2  33508  1arithidom  33509  dimkerim  33661  lvecendof1f1o  33667  fldextrspunlsplem  33707  nn0constr  33795  constraddcl  33796  constrnegcl  33797  constrremulcl  33801  constrrecl  33803  constrimcl  33804  constrmulcl  33805  constrreinvcl  33806  constrinvcl  33807  constrresqrtcl  33811  constrabscl  33812  2sqr3minply  33814  submatminr1  33844  mdetpmtr1  33857  madjusmdetlem1  33861  zarcmplem  33915  qqhnm  34024  esumfzf  34103  ddemeas  34270  sseqp1  34429  ballotlemi1  34537  ballotlemii  34538  ballotlemic  34541  ballotlem1c  34542  fsum2dsub  34641  circlemeth  34674  hgt750lemb  34690  hgt750lema  34691  hgt750leme  34692  elmrsubrn  35585  cos2h  37671  itg2addnclem  37731  itgmulc2nclem2  37747  areacirclem1  37768  areacirclem4  37771  cntotbnd  37856  atmod2i2  39981  trljat1  40285  trljat2  40286  cdleme9  40372  cdleme15b  40394  cdleme20c  40430  cdleme22eALTN  40464  dvhopN  41235  doca2N  41245  cdlemn10  41325  dochocss  41485  djhlj  41520  dihprrnlem1N  41543  dihprrnlem2  41544  lcfl7lem  41618  lclkrlem2c  41628  hgmapadd  42013  hdmapinvlem3  42039  hgmapvvlem1  42042  sumcubes  42431  zaddcomlem  42581  fidomncyc  42653  selvvvval  42703  rmydbl  43057  jm2.18  43105  jm2.19  43110  proot1hash  43312  dssmapnvod  44137  binomcxplemnotnn0  44473  oddfl  45403  dstregt0  45407  supsubc  45476  absimlere  45601  uzinico2  45685  mccllem  45721  ellimcabssub0  45741  sumnnodd  45754  climresmpt  45781  limsupresuz  45825  liminfresuz  45906  coskpi2  45988  cosknegpi  45991  dvsinax  46035  dvnmptdivc  46060  dvnxpaek  46064  dvnmul  46065  dvmptfprodlem  46066  ditgeqiooicc  46082  itgioocnicc  46099  itgspltprt  46101  wallispi2lem2  46194  dirkerper  46218  dirkertrigeqlem2  46221  dirkertrigeqlem3  46222  dirkertrigeq  46223  dirkercncflem2  46226  dirkercncflem4  46228  fourierdlem18  46247  fourierdlem19  46248  fourierdlem33  46262  fourierdlem35  46264  fourierdlem41  46270  fourierdlem42  46271  fourierdlem48  46276  fourierdlem49  46277  fourierdlem50  46278  fourierdlem53  46281  fourierdlem63  46291  fourierdlem65  46293  fourierdlem73  46301  fourierdlem74  46302  fourierdlem75  46303  fourierdlem81  46309  fourierdlem82  46310  fourierdlem83  46311  fourierdlem84  46312  fourierdlem90  46318  fourierdlem93  46321  fourierdlem95  46323  fourierdlem103  46331  fourierdlem104  46332  fourierdlem107  46335  fourierdlem111  46339  fourierswlem  46352  fouriersw  46353  etransclem4  46360  etransclem9  46365  etransclem28  46384  etransclem35  46391  etransclem38  46394  sge0tsms  46502  sge0sup  46513  sge0resplit  46528  sge0split  46531  sge0ss  46534  sge0rpcpnf  46543  sge0isum  46549  sge0xadd  46557  sge0seq  46568  ismeannd  46589  caratheodorylem1  46648  isomenndlem  46652  hoicvrrex  46678  ovn0lem  46687  hoidmvlelem2  46718  hoidmvlelem3  46719  ovnlecvr2  46732  voncmpl  46743  hspmbllem1  46748  hspmbllem2  46749  ovolval4lem1  46771  incsmf  46864  smfpimltmpt  46868  smfpimltxrmptf  46880  decsmf  46889  smfpimgtmpt  46903  smfpimgtxrmptf  46906  smfmullem1  46913  smflimsuplem2  46943  sigarac  46974  cevathlem2  46990  m1modmmod  47482  fmtnorec3  47672  fmtnorec4  47673  oddflALTV  47787  perfectALTVlem2  47846  nnsum4primeseven  47924  nnsum4primesevenALTV  47925  uspgrlimlem1  48112  gpgvtxedg0  48187  gpgvtxedg1  48188  gpg3kgrtriexlem2  48208  ply1mulgsum  48515  lindslinindsimp2lem5  48587  nn0sumshdiglemA  48744  nn0sumshdiglemB  48745  nn0sumshdiglem2  48747  itschlc0yqe  48885