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

Theorem syl5req 2328
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 2327 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2288 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  syl5reqr  2330  opeqsn  4262  ordintdif  4441  relop  4834  funopg  5286  funcnvres  5321  nneob  6650  sucdom2  7057  unblem2  7110  pwfilem  7150  kmlem2  7777  kmlem11  7786  kmlem12  7787  cflim3  7888  1idsr  8720  recextlem1  9398  nn0supp  10017  quoremz  10959  quoremnn0ALT  10961  intfrac2  10962  hashprg  11368  hashfacen  11392  leiso  11397  cvgcmpce  12276  explecnv  12323  ramub1lem1  13073  ressress  13205  subsubc  13727  efginvrel2  15036  efgredleme  15052  efgcpbllemb  15064  frgpnabllem1  15161  gsumzmhm  15210  dprd2da  15277  dpjcntz  15287  dpjdisj  15288  dpjlsm  15289  dpjidcl  15293  ablfac1lem  15303  ablfac1eu  15308  lmhmlsp  15806  mplmon2mul  16242  fixufil  17617  nmfval2  18113  nmval2  18114  rerest  18310  xrrest  18313  xrge0gsumle  18338  voliunlem3  18909  volsup  18913  itg1addlem5  19055  itg2monolem1  19105  itg2cnlem2  19117  itgmpt  19137  iblcnlem1  19142  itgcnlem  19144  itgioo  19170  limcres  19236  mdegfval  19448  dgrlem  19611  coeidlem  19619  mcubic  20143  binom4  20146  dquartlem2  20148  amgm  20285  wilthlem2  20307  rpvmasum2  20661  pntlemo  20756  opidon2  20991  vc2  21111  nvge0  21240  nmoo0  21369  bcsiALT  21758  pjchi  22011  shjshseli  22072  spanpr  22159  pjinvari  22771  mdslmd1lem2  22906  iundifdifd  23159  iundifdif  23160  gtiso  23241  esumpr2  23439  dvreasin  24923  preoran2  25230  iscom  25333  ununr  25420  dualalg  25782  topjoin  26314  tailfval  26321  tailf  26324  elrfi  26769  fzsplit1nn0  26833  rabdiophlem2  26883  eldioph4b  26894  diophren  26896  pell1qrgaplem  26958  rngunsnply  27378  psgnunilem1  27416  compne  27642  fmuldfeq  27713  stoweidlem44  27793  cdleme4  30427  cdleme22e  30533  cdleme22eALTN  30534  cdleme42a  30660  cdleme42d  30662  cdlemk20  31063  dih1dimatlem0  31518  lcfrlem2  31733
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator