MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5req Structured version   Unicode version

Theorem syl5req 2521
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl5req.1  |-  A  =  B
syl5req.2  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
syl5req  |-  ( ph  ->  C  =  A )

Proof of Theorem syl5req
StepHypRef Expression
1 syl5req.1 . . 3  |-  A  =  B
2 syl5req.2 . . 3  |-  ( ph  ->  B  =  C )
31, 2syl5eq 2520 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2475 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  syl5reqr  2523  opeqsn  4743  ordintdif  4927  relop  5151  funopg  5618  funcnvres  5655  csbriota  6255  mpt2curryd  6995  nneob  7298  sucdom2  7711  unblem2  7769  pwfilem  7810  kmlem2  8527  kmlem11  8536  kmlem12  8537  cflim3  8638  1idsr  9471  recextlem1  10175  nn0suppOLD  10846  quoremz  11946  quoremnn0ALT  11948  intfrac2  11949  hashprg  12424  hashfacen  12465  leiso  12470  swrdccat3a  12678  repsw2  12847  repsw3  12848  cvgcmpce  13591  explecnv  13635  ramub1lem1  14399  ressress  14548  subsubc  15076  psgnunilem1  16314  psgn0fv0  16332  psgnsn  16341  efginvrel2  16541  efgredleme  16557  efgcpbllemb  16569  frgpnabllem1  16668  gsumzaddlem  16725  gsumzmhm  16748  gsumzmhmOLD  16749  fsfnn0gsumfsffz  16802  dprd2da  16881  dpjcntz  16891  dpjdisj  16892  dpjlsm  16893  dpjidcl  16897  dpjidclOLD  16904  ablfac1lem  16909  ablfac1eu  16914  lmhmlsp  17478  mplmon2mul  17937  frlmip  18576  1marepvmarrepid  18844  m1detdiag  18866  cramerimplem2  18953  pmatcollpw3lem  19051  chpscmatgsumbin  19112  chpscmatgsummon  19113  cayhamlem2  19152  neitr  19447  fixufil  20158  trust  20467  restmetu  20825  nmfval2  20846  nmval2  20847  rerest  21044  xrrest  21047  xrge0gsumle  21073  rrxip  21557  voliunlem3  21697  volsup  21701  itg1addlem5  21842  itg2monolem1  21892  itg2cnlem2  21904  itgmpt  21924  iblcnlem1  21929  itgcnlem  21931  itgioo  21957  limcres  22025  mdegfval  22195  dgrlem  22361  coeidlem  22369  mcubic  22906  binom4  22909  dquartlem2  22911  amgm  23048  wilthlem2  23071  rpvmasum2  23425  pntlemo  23520  wlkntrllem3  24239  frgrancvvdeqlem4  24710  opidon2  25002  vc2  25124  nvge0  25253  nmoo0  25382  bcsiALT  25772  pjchi  26026  shjshseli  26087  spanpr  26174  pjinvari  26786  mdslmd1lem2  26921  iundifdifd  27102  iundifdif  27103  gtiso  27191  rngurd  27441  esumpr2  27714  eulerpartlemt  27950  ofcccat  28138  lgamgulmlem2  28212  eflgam  28227  risefallfac  28723  dvasin  29680  dvacos  29681  topjoin  29786  tailfval  29793  tailf  29796  elrfi  30230  fzsplit1nn0  30291  rabdiophlem2  30339  eldioph4b  30349  diophren  30351  pell1qrgaplem  30413  rngunsnply  30727  compne  30927  fmuldfeq  31133  itgiccshift  31298  stoweidlem44  31344  fourierdlem60  31467  fourierdlem68  31475  fourierdlem111  31518  fourierswlem  31531  fsumsplitsndif  31815  cdleme4  35034  cdleme22e  35140  cdleme22eALTN  35141  cdleme42a  35267  cdleme42d  35269  cdlemk20  35670  dih1dimatlem0  36125  lcfrlem2  36340
  Copyright terms: Public domain W3C validator