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

Theorem 3eqtrrd 2648
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 2643 . 2 (𝜑𝐴 = 𝐶)
4 3eqtrd.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtr2d 2644 1 (𝜑𝐷 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602
This theorem is referenced by:  fimacnvinrn  6241  fvcofneq  6260  iunfictbso  8797  axcnre  9841  fseq1p1m1  12238  seqf1olem1  12657  expmulz  12723  expubnd  12738  subsq  12789  bcm1k  12919  bcpasc  12925  cshwcshid  13370  crim  13649  rereb  13654  rlimrecl  14105  iseraltlem2  14207  fsumparts  14325  isumshft  14356  geoserg  14383  efsub  14615  sincossq  14691  efieq1re  14714  eucalg  15084  lcmfunsnlem  15138  phiprmpw  15265  modprmn0modprm0  15296  coprimeprodsq  15297  pythagtriplem15  15318  pythagtriplem17  15320  fldivp1  15385  1arithlem4  15414  setsidvald  15667  setsid  15688  pwsbas  15916  invfuc  16403  latdisdlem  16958  odinv  17747  frgpuplem  17954  gexexlem  18024  srgbinomlem4  18312  gsumdixp  18378  mplcoe1  19232  evlsvarsrng  19295  ply1idvr1  19430  ply1coe  19433  evls1varsrng  19471  cnfldsub  19539  mat1scmat  20106  m1detdiag  20164  mdetunilem7  20185  madugsum  20210  pm2mpmhmlem2  20385  mretopd  20648  upxp  21178  uptx  21180  imasdsf1olem  21929  clmvs2  22633  itgmulc2lem2  23322  r1pid  23640  coeeulem  23701  fta1lem  23783  aaliou3lem8  23821  eff1olem  24015  tanarg  24086  logcnlem4  24108  root1cj  24214  angpieqvdlem  24272  quad2  24283  dcubic  24290  quart1  24300  jensen  24432  lgamgulmlem5  24476  lgamgulm2  24479  ftalem5  24520  basellem8  24531  chpchtsum  24661  logfaclbnd  24664  perfectlem2  24672  gausslemma2dlem1a  24807  2sqlem3  24862  dchrvmasum2lem  24902  dchrvmasumiflem2  24908  selberglem2  24952  selberg3r  24975  pntlem3  25015  ostth2  25043  ostth3  25044  krippenlem  25303  colinearalglem1  25504  axlowdimlem16  25555  axcontlem4  25565  nmbdoplbi  28073  nmcopexi  28076  nmbdfnlbi  28098  nmcfnexi  28100  nmcfnlbi  28101  hstoh  28281  fcobij  28694  lt2addrd  28709  xlt2addrd  28719  isarchi3  28878  archirngz  28880  symgfcoeu  28982  submatminr1  29010  mdetpmtr1  29023  madjusmdetlem1  29027  qqhnm  29168  esumfzf  29264  ddemeas  29432  sseqp1  29590  ballotlemi1  29697  ballotlemii  29698  ballotlemic  29701  ballotlem1c  29702  elmrsubrn  30477  cos2h  32366  itg2addnclem  32427  itgmulc2nclem2  32443  areacirclem1  32466  areacirclem4  32469  cntotbnd  32561  atmod2i2  33962  trljat1  34267  trljat2  34268  cdleme9  34354  cdleme15b  34376  cdleme20c  34413  cdleme22eALTN  34447  dvhopN  35219  doca2N  35229  cdlemn10  35309  dochocss  35469  djhlj  35504  dihprrnlem1N  35527  dihprrnlem2  35528  lcfl7lem  35602  lclkrlem2c  35612  hgmapadd  36000  hdmapinvlem3  36026  hgmapvvlem1  36029  rmydbl  36319  jm2.18  36369  jm2.19  36374  proot1hash  36593  dssmapnvod  37130  binomcxplemnotnn0  37373  oddfl  38226  dstregt0  38230  supsubc  38307  fsumsplit1  38436  mccllem  38461  ellimcabssub0  38481  sumnnodd  38494  climresmpt  38523  coskpi2  38546  cosknegpi  38549  dvsinax  38598  dvnmptdivc  38625  dvnxpaek  38629  dvnmul  38630  dvmptfprodlem  38631  ditgeqiooicc  38649  itgioocnicc  38666  itgspltprt  38668  wallispi2lem2  38762  dirkerper  38786  dirkertrigeqlem2  38789  dirkertrigeqlem3  38790  dirkertrigeq  38791  dirkercncflem2  38794  dirkercncflem4  38796  fourierdlem18  38815  fourierdlem19  38816  fourierdlem33  38830  fourierdlem35  38832  fourierdlem41  38838  fourierdlem42  38839  fourierdlem48  38844  fourierdlem49  38845  fourierdlem50  38846  fourierdlem53  38849  fourierdlem63  38859  fourierdlem65  38861  fourierdlem73  38869  fourierdlem74  38870  fourierdlem75  38871  fourierdlem81  38877  fourierdlem82  38878  fourierdlem83  38879  fourierdlem84  38880  fourierdlem90  38886  fourierdlem93  38889  fourierdlem95  38891  fourierdlem103  38899  fourierdlem104  38900  fourierdlem107  38903  fourierdlem111  38907  fourierswlem  38920  fouriersw  38921  etransclem4  38928  etransclem9  38933  etransclem28  38952  etransclem35  38959  etransclem38  38962  sge0tsms  39070  sge0sup  39081  sge0resplit  39096  sge0split  39099  sge0ss  39102  sge0rpcpnf  39111  sge0isum  39117  sge0xadd  39125  sge0seq  39136  ismeannd  39157  caratheodorylem1  39213  isomenndlem  39217  hoicvrrex  39243  ovn0lem  39252  hoidmvlelem2  39283  hoidmvlelem3  39284  ovnlecvr2  39297  voncmpl  39308  hspmbllem1  39313  hspmbllem2  39314  ovolval4lem1  39336  incsmf  39426  smfpimltmpt  39430  smfpimltxrmpt  39442  decsmf  39450  smfpimgtmpt  39464  smfpimgtxrmpt  39467  smfmullem1  39473  sigarac  39487  cevathlem2  39503  fmtnorec3  39796  fmtnorec4  39797  pwdif  39837  oddflALTV  39911  perfectALTVlem2  39963  nnsum4primeseven  40014  nnsum4primesevenALTV  40015  c0snmgmhm  41699  funcrngcsetc  41785  funcringcsetc  41822  ply1mulgsum  41967  lindslinindsimp2lem5  42040  m1modmmod  42105  nn0sumshdiglemA  42206  nn0sumshdiglemB  42207  nn0sumshdiglem2  42209
  Copyright terms: Public domain W3C validator