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

Theorem syl5req 2403
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 2402 . 2  |-  ( ph  ->  A  =  C )
43eqcomd 2363 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642
This theorem is referenced by:  syl5reqr  2405  opeqsn  4344  ordintdif  4523  relop  4916  funopg  5368  funcnvres  5403  nneob  6737  sucdom2  7145  unblem2  7200  pwfilem  7240  kmlem2  7867  kmlem11  7876  kmlem12  7877  cflim3  7978  1idsr  8810  recextlem1  9488  nn0supp  10109  quoremz  11051  quoremnn0ALT  11053  intfrac2  11054  hashprg  11464  hashfacen  11488  leiso  11493  cvgcmpce  12373  explecnv  12420  ramub1lem1  13170  ressress  13302  subsubc  13826  efginvrel2  15135  efgredleme  15151  efgcpbllemb  15163  frgpnabllem1  15260  gsumzmhm  15309  dprd2da  15376  dpjcntz  15386  dpjdisj  15387  dpjlsm  15388  dpjidcl  15392  ablfac1lem  15402  ablfac1eu  15407  lmhmlsp  15905  mplmon2mul  16341  fixufil  17719  nmfval2  18215  nmval2  18216  rerest  18412  xrrest  18415  xrge0gsumle  18441  voliunlem3  19013  volsup  19017  itg1addlem5  19159  itg2monolem1  19209  itg2cnlem2  19221  itgmpt  19241  iblcnlem1  19246  itgcnlem  19248  itgioo  19274  limcres  19340  mdegfval  19552  dgrlem  19715  coeidlem  19723  mcubic  20254  binom4  20257  dquartlem2  20259  amgm  20396  wilthlem2  20419  rpvmasum2  20773  pntlemo  20868  opidon2  21103  vc2  21225  nvge0  21354  nmoo0  21483  bcsiALT  21872  pjchi  22125  shjshseli  22186  spanpr  22273  pjinvari  22885  mdslmd1lem2  23020  iundifdifd  23211  iundifdif  23212  gtiso  23292  trust  23533  restmetu  23615  esumpr2  23724  lgamgulmlem2  24063  eflgam  24078  risefallfac  24640  dvreasin  25515  topjoin  25638  tailfval  25645  tailf  25648  elrfi  26092  fzsplit1nn0  26156  rabdiophlem2  26206  eldioph4b  26217  diophren  26219  pell1qrgaplem  26281  rngunsnply  26701  psgnunilem1  26739  compne  26965  fmuldfeq  27036  stoweidlem44  27116  wlkntrllem5  27705  frgrancvvdeqlem4  27866  cdleme4  30496  cdleme22e  30602  cdleme22eALTN  30603  cdleme42a  30729  cdleme42d  30731  cdlemk20  31132  dih1dimatlem0  31587  lcfrlem2  31802
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2351
  Copyright terms: Public domain W3C validator