Theorem 3eqtrrd 2771

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 2766	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtrd.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2767	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 2121  ax-ext 2703

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

This theorem is referenced by:  fimacnvinrn  7004  fvcofneq  7026  iunfictbso  10005  axcnre  11055  fseq1p1m1  13498  seqf1olem1  13948  expmulz  14015  expubnd  14085  subsq  14117  bcm1k  14222  bcpasc  14228  cshwcshid  14734  crim  15022  rereb  15027  rlimrecl  15487  iseraltlem2  15590  fsumsplit1  15652  fsumparts  15713  isumshft  15746  geoserg  15773  pwdif  15775  efsub  16009  sincossq  16085  efieq1re  16108  nn0expgcd  16475  eucalg  16498  lcmfunsnlem  16552  phiprmpw  16687  modprmn0modprm0  16719  coprimeprodsq  16720  pythagtriplem15  16741  pythagtriplem17  16743  fldivp1  16809  1arithlem4  16838  setsidvald  17110  setsid  17118  pwsbas  17391  invfuc  17884  estrreslem1  18043  latdisdlem  18402  ghmquskerco  19196  odinv  19473  frgpuplem  19684  gexexlem  19764  fincygsubgodd  20026  srgbinomlem4  20147  gsumdixp  20237  c0snmgmhm  20380  funcrngcsetc  20555  funcringcsetc  20589  cnfldsub  21334  mplcoe1  21972  evlsvarsrng  22034  psdmul  22081  ply1idvr1OLD  22210  ply1coe  22213  evls1varsrng  22255  mat1scmat  22454  m1detdiag  22512  mdetunilem7  22533  madugsum  22558  pm2mpmhmlem2  22734  mretopd  23007  upxp  23538  uptx  23540  imasdsf1olem  24288  clmvs2  25021  cphipipcj  25127  cphipval2  25168  itgmulc2lem2  25761  r1pid  26093  coeeulem  26156  fta1lem  26242  aaliou3lem8  26280  eff1olem  26484  tanarg  26555  logcnlem4  26581  root1cj  26693  angpieqvdlem  26765  quad2  26776  dcubic  26783  quart1  26793  jensen  26926  lgamgulmlem5  26970  lgamgulm2  26973  ftalem5  27014  basellem8  27025  chpchtsum  27157  logfaclbnd  27160  perfectlem2  27168  gausslemma2dlem1a  27303  2sqlem3  27358  dchrvmasum2lem  27434  dchrvmasumiflem2  27440  selberglem2  27484  selberg3r  27507  pntlem3  27547  ostth2  27575  ostth3  27576  madeoldsuc  27830  zseo  28345  addhalfcut  28379  pw2cut2  28382  krippenlem  28668  colinearalglem1  28884  axlowdimlem16  28935  axcontlem4  28945  clwlkclwwlkfo  29989  nmbdoplbi  32004  nmcopexi  32007  nmbdfnlbi  32029  nmcfnexi  32031  nmcfnlbi  32032  hstoh  32212  fcobij  32703  lt2addrd  32734  xlt2addrd  32742  cshwrnid  32942  symgfcoeu  33051  cycpmconjslem2  33124  cycpmconjs  33125  isarchi3  33156  archirngz  33158  elrgspnsubrunlem1  33214  elrspunsn  33394  mxidlirredi  33436  1arithidomlem1  33500  1arithidomlem2  33501  1arithidom  33502  dimkerim  33640  lvecendof1f1o  33646  fldextrspunlsplem  33686  nn0constr  33774  constraddcl  33775  constrnegcl  33776  constrremulcl  33780  constrrecl  33782  constrimcl  33783  constrmulcl  33784  constrreinvcl  33785  constrinvcl  33786  constrresqrtcl  33790  constrabscl  33791  2sqr3minply  33793  submatminr1  33823  mdetpmtr1  33836  madjusmdetlem1  33840  zarcmplem  33894  qqhnm  34003  esumfzf  34082  ddemeas  34249  sseqp1  34408  ballotlemi1  34516  ballotlemii  34517  ballotlemic  34520  ballotlem1c  34521  fsum2dsub  34620  circlemeth  34653  hgt750lemb  34669  hgt750lema  34670  hgt750leme  34671  elmrsubrn  35564  cos2h  37661  itg2addnclem  37721  itgmulc2nclem2  37737  areacirclem1  37758  areacirclem4  37761  cntotbnd  37846  atmod2i2  39971  trljat1  40275  trljat2  40276  cdleme9  40362  cdleme15b  40384  cdleme20c  40420  cdleme22eALTN  40454  dvhopN  41225  doca2N  41235  cdlemn10  41315  dochocss  41475  djhlj  41510  dihprrnlem1N  41533  dihprrnlem2  41534  lcfl7lem  41608  lclkrlem2c  41618  hgmapadd  42003  hdmapinvlem3  42029  hgmapvvlem1  42032  sumcubes  42416  zaddcomlem  42566  fidomncyc  42638  selvvvval  42688  rmydbl  43043  jm2.18  43091  jm2.19  43096  proot1hash  43298  dssmapnvod  44123  binomcxplemnotnn0  44459  oddfl  45389  dstregt0  45393  supsubc  45462  absimlere  45587  uzinico2  45671  mccllem  45707  ellimcabssub0  45727  sumnnodd  45740  climresmpt  45767  limsupresuz  45811  liminfresuz  45892  coskpi2  45974  cosknegpi  45977  dvsinax  46021  dvnmptdivc  46046  dvnxpaek  46050  dvnmul  46051  dvmptfprodlem  46052  ditgeqiooicc  46068  itgioocnicc  46085  itgspltprt  46087  wallispi2lem2  46180  dirkerper  46204  dirkertrigeqlem2  46207  dirkertrigeqlem3  46208  dirkertrigeq  46209  dirkercncflem2  46212  dirkercncflem4  46214  fourierdlem18  46233  fourierdlem19  46234  fourierdlem33  46248  fourierdlem35  46250  fourierdlem41  46256  fourierdlem42  46257  fourierdlem48  46262  fourierdlem49  46263  fourierdlem50  46264  fourierdlem53  46267  fourierdlem63  46277  fourierdlem65  46279  fourierdlem73  46287  fourierdlem74  46288  fourierdlem75  46289  fourierdlem81  46295  fourierdlem82  46296  fourierdlem83  46297  fourierdlem84  46298  fourierdlem90  46304  fourierdlem93  46307  fourierdlem95  46309  fourierdlem103  46317  fourierdlem104  46318  fourierdlem107  46321  fourierdlem111  46325  fourierswlem  46338  fouriersw  46339  etransclem4  46346  etransclem9  46351  etransclem28  46370  etransclem35  46377  etransclem38  46380  sge0tsms  46488  sge0sup  46499  sge0resplit  46514  sge0split  46517  sge0ss  46520  sge0rpcpnf  46529  sge0isum  46535  sge0xadd  46543  sge0seq  46554  ismeannd  46575  caratheodorylem1  46634  isomenndlem  46638  hoicvrrex  46664  ovn0lem  46673  hoidmvlelem2  46704  hoidmvlelem3  46705  ovnlecvr2  46718  voncmpl  46729  hspmbllem1  46734  hspmbllem2  46735  ovolval4lem1  46757  incsmf  46850  smfpimltmpt  46854  smfpimltxrmptf  46866  decsmf  46875  smfpimgtmpt  46889  smfpimgtxrmptf  46892  smfmullem1  46899  smflimsuplem2  46929  sigarac  46960  cevathlem2  46976  m1modmmod  47468  fmtnorec3  47658  fmtnorec4  47659  oddflALTV  47773  perfectALTVlem2  47832  nnsum4primeseven  47910  nnsum4primesevenALTV  47911  uspgrlimlem1  48098  gpgvtxedg0  48173  gpgvtxedg1  48174  gpg3kgrtriexlem2  48194  ply1mulgsum  48501  lindslinindsimp2lem5  48573  nn0sumshdiglemA  48730  nn0sumshdiglemB  48731  nn0sumshdiglem2  48733  itschlc0yqe  48871