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

Theorem sps 1865
Description: Generalization of antecedent. (Contributed by NM, 5-Jan-1993.)
Hypothesis
Ref Expression
sps.1
Assertion
Ref Expression
sps

Proof of Theorem sps
StepHypRef Expression
1 sp 1859 . 2
2 sps.1 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393
This theorem is referenced by:  2sp  1866  19.2g  1868  axc112  1937  ax12v2  2083  equveli  2088  dfsb2  2114  drsb1  2118  drsb2  2119  nfsb4t  2130  sbi1  2133  sbco2  2158  sbco3  2160  sb9  2169  sbal1  2204  eujustALT  2285  mo3OLD  2324  2eu6  2383  ralcom2  3022  ceqsalgALT  3135  reu6  3288  sbcal  3379  reldisj  3870  dfnfc2  4267  eusvnfb  4648  nfnid  4681  mosubopt  4750  dfid3  4801  issref  5385  fv3  5884  fvmptt  5971  fnoprabg  6403  pssnn  7758  kmlem16  8566  nd3  8985  axunndlem1  8991  axunnd  8992  axpowndlem1  8993  axpowndlem3OLD  8997  axregndlem1  9000  axregndlem2  9001  axregndOLD  9003  axacndlem5  9010  bwthOLD  19911  fundmpss  29196  wfrlem5  29347  frrlem5  29391  nalf  29868  unisym1  29888  wl-nfimf1  29978  wl-dral1d  29984  wl-nfs1t  29991  wl-sb8t  30000  wl-sbhbt  30002  wl-equsb4  30005  wl-sbalnae  30012  wl-mo3t  30021  wl-ax11-lem5  30029  wl-ax11-lem8  30032  wl-sbcom3  30035  pm11.57  31295  axc5c4c711toc7  31311  axc11next  31313  pm14.122b  31330  dropab1  31356  dropab2  31357  ax6e2eq  33330  bj-axc15v  34330
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator