MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtrrd Structured version   Visualization version   GIF version

Theorem 3eqtrrd 2690
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
StepHypRef Expression
1 3eqtrd.1 . . 3 (𝜑𝐴 = 𝐵)
2 3eqtrd.2 . . 3 (𝜑𝐵 = 𝐶)
31, 2eqtrd 2685 . 2 (𝜑𝐴 = 𝐶)
4 3eqtrd.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtr2d 2686 1 (𝜑𝐷 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  fimacnvinrn  6388  fvcofneq  6407  iunfictbso  8975  axcnre  10023  fseq1p1m1  12452  seqf1olem1  12880  expmulz  12946  expubnd  12961  subsq  13012  bcm1k  13142  bcpasc  13148  cshwcshid  13619  crim  13899  rereb  13904  rlimrecl  14355  iseraltlem2  14457  fsumparts  14582  isumshft  14615  geoserg  14642  efsub  14874  sincossq  14950  efieq1re  14973  eucalg  15347  lcmfunsnlem  15401  phiprmpw  15528  modprmn0modprm0  15559  coprimeprodsq  15560  pythagtriplem15  15581  pythagtriplem17  15583  fldivp1  15648  1arithlem4  15677  setsidvald  15936  setsid  15961  pwsbas  16194  invfuc  16681  latdisdlem  17236  odinv  18024  frgpuplem  18231  gexexlem  18301  srgbinomlem4  18589  gsumdixp  18655  mplcoe1  19513  evlsvarsrng  19576  ply1idvr1  19711  ply1coe  19714  evls1varsrng  19752  cnfldsub  19822  mat1scmat  20393  m1detdiag  20451  mdetunilem7  20472  madugsum  20497  pm2mpmhmlem2  20672  mretopd  20944  upxp  21474  uptx  21476  imasdsf1olem  22225  clmvs2  22940  cphipipcj  23046  cphipval2  23086  itgmulc2lem2  23644  r1pid  23964  coeeulem  24025  fta1lem  24107  aaliou3lem8  24145  eff1olem  24339  tanarg  24410  logcnlem4  24436  root1cj  24542  angpieqvdlem  24600  quad2  24611  dcubic  24618  quart1  24628  jensen  24760  lgamgulmlem5  24804  lgamgulm2  24807  ftalem5  24848  basellem8  24859  chpchtsum  24989  logfaclbnd  24992  perfectlem2  25000  gausslemma2dlem1a  25135  2sqlem3  25190  dchrvmasum2lem  25230  dchrvmasumiflem2  25236  selberglem2  25280  selberg3r  25303  pntlem3  25343  ostth2  25371  ostth3  25372  krippenlem  25630  colinearalglem1  25831  axlowdimlem16  25882  axcontlem4  25892  nmbdoplbi  29011  nmcopexi  29014  nmbdfnlbi  29036  nmcfnexi  29038  nmcfnlbi  29039  hstoh  29219  fcobij  29628  lt2addrd  29644  xlt2addrd  29651  isarchi3  29869  archirngz  29871  symgfcoeu  29973  submatminr1  30004  mdetpmtr1  30017  madjusmdetlem1  30021  qqhnm  30162  esumfzf  30259  ddemeas  30427  sseqp1  30585  ballotlemi1  30692  ballotlemii  30693  ballotlemic  30696  ballotlem1c  30697  fsum2dsub  30813  circlemeth  30846  hgt750lemb  30862  hgt750lema  30863  hgt750leme  30864  elmrsubrn  31543  cos2h  33530  itg2addnclem  33591  itgmulc2nclem2  33607  areacirclem1  33630  areacirclem4  33633  cntotbnd  33725  atmod2i2  35466  trljat1  35771  trljat2  35772  cdleme9  35858  cdleme15b  35880  cdleme20c  35916  cdleme22eALTN  35950  dvhopN  36722  doca2N  36732  cdlemn10  36812  dochocss  36972  djhlj  37007  dihprrnlem1N  37030  dihprrnlem2  37031  lcfl7lem  37105  lclkrlem2c  37115  hgmapadd  37503  hdmapinvlem3  37529  hgmapvvlem1  37532  rmydbl  37822  jm2.18  37872  jm2.19  37877  proot1hash  38095  dssmapnvod  38631  binomcxplemnotnn0  38872  oddfl  39803  dstregt0  39807  supsubc  39882  absimlere  40023  uzinico2  40107  fsumsplit1  40122  mccllem  40147  ellimcabssub0  40167  sumnnodd  40180  climresmpt  40209  limsupresuz  40253  liminfresuz  40334  coskpi2  40395  cosknegpi  40398  dvsinax  40445  dvnmptdivc  40471  dvnxpaek  40475  dvnmul  40476  dvmptfprodlem  40477  ditgeqiooicc  40494  itgioocnicc  40511  itgspltprt  40513  wallispi2lem2  40607  dirkerper  40631  dirkertrigeqlem2  40634  dirkertrigeqlem3  40635  dirkertrigeq  40636  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem18  40660  fourierdlem19  40661  fourierdlem33  40675  fourierdlem35  40677  fourierdlem41  40683  fourierdlem42  40684  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem53  40694  fourierdlem63  40704  fourierdlem65  40706  fourierdlem73  40714  fourierdlem74  40715  fourierdlem75  40716  fourierdlem81  40722  fourierdlem82  40723  fourierdlem83  40724  fourierdlem84  40725  fourierdlem90  40731  fourierdlem93  40734  fourierdlem95  40736  fourierdlem103  40744  fourierdlem104  40745  fourierdlem107  40748  fourierdlem111  40752  fourierswlem  40765  fouriersw  40766  etransclem4  40773  etransclem9  40778  etransclem28  40797  etransclem35  40804  etransclem38  40807  sge0tsms  40915  sge0sup  40926  sge0resplit  40941  sge0split  40944  sge0ss  40947  sge0rpcpnf  40956  sge0isum  40962  sge0xadd  40970  sge0seq  40981  ismeannd  41002  caratheodorylem1  41061  isomenndlem  41065  hoicvrrex  41091  ovn0lem  41100  hoidmvlelem2  41131  hoidmvlelem3  41132  ovnlecvr2  41145  voncmpl  41156  hspmbllem1  41161  hspmbllem2  41162  ovolval4lem1  41184  incsmf  41272  smfpimltmpt  41276  smfpimltxrmpt  41288  decsmf  41296  smfpimgtmpt  41310  smfpimgtxrmpt  41313  smfmullem1  41319  smfsupmpt  41342  smfinfmpt  41346  smflimsuplem2  41348  sigarac  41362  cevathlem2  41378  fmtnorec3  41785  fmtnorec4  41786  pwdif  41826  oddflALTV  41900  perfectALTVlem2  41956  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  c0snmgmhm  42239  funcrngcsetc  42323  funcringcsetc  42360  ply1mulgsum  42503  lindslinindsimp2lem5  42576  m1modmmod  42641  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739  nn0sumshdiglem2  42741
  Copyright terms: Public domain W3C validator