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

Theorem syl5req 2341
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 2340 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2301 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  syl5reqr  2343  opeqsn  4278  ordintdif  4457  relop  4850  funopg  5302  funcnvres  5337  nneob  6666  sucdom2  7073  unblem2  7126  pwfilem  7166  kmlem2  7793  kmlem11  7802  kmlem12  7803  cflim3  7904  1idsr  8736  recextlem1  9414  nn0supp  10033  quoremz  10975  quoremnn0ALT  10977  intfrac2  10978  hashprg  11384  hashfacen  11408  leiso  11413  cvgcmpce  12292  explecnv  12339  ramub1lem1  13089  ressress  13221  subsubc  13743  efginvrel2  15052  efgredleme  15068  efgcpbllemb  15080  frgpnabllem1  15177  gsumzmhm  15226  dprd2da  15293  dpjcntz  15303  dpjdisj  15304  dpjlsm  15305  dpjidcl  15309  ablfac1lem  15319  ablfac1eu  15324  lmhmlsp  15822  mplmon2mul  16258  fixufil  17633  nmfval2  18129  nmval2  18130  rerest  18326  xrrest  18329  xrge0gsumle  18354  voliunlem3  18925  volsup  18929  itg1addlem5  19071  itg2monolem1  19121  itg2cnlem2  19133  itgmpt  19153  iblcnlem1  19158  itgcnlem  19160  itgioo  19186  limcres  19252  mdegfval  19464  dgrlem  19627  coeidlem  19635  mcubic  20159  binom4  20162  dquartlem2  20164  amgm  20301  wilthlem2  20323  rpvmasum2  20677  pntlemo  20772  opidon2  21007  vc2  21127  nvge0  21256  nmoo0  21385  bcsiALT  21774  pjchi  22027  shjshseli  22088  spanpr  22175  pjinvari  22787  mdslmd1lem2  22922  iundifdifd  23175  iundifdif  23176  gtiso  23256  esumpr2  23454  dvreasin  25026  preoran2  25333  iscom  25436  ununr  25523  dualalg  25885  topjoin  26417  tailfval  26424  tailf  26427  elrfi  26872  fzsplit1nn0  26936  rabdiophlem2  26986  eldioph4b  26997  diophren  26999  pell1qrgaplem  27061  rngunsnply  27481  psgnunilem1  27519  compne  27745  fmuldfeq  27816  stoweidlem44  27896  wlkntrllem5  28349  cdleme4  31049  cdleme22e  31155  cdleme22eALTN  31156  cdleme42a  31282  cdleme42d  31284  cdlemk20  31685  dih1dimatlem0  32140  lcfrlem2  32355
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator