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

Theorem sps 1851
Description: Generalization of antecedent. (Contributed by NM, 5-Jan-1993.)
Hypothesis
Ref Expression
sps.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
sps  |-  ( A. x ph  ->  ps )

Proof of Theorem sps
StepHypRef Expression
1 sp 1845 . 2  |-  ( A. x ph  ->  ph )
2 sps.1 . 2  |-  ( ph  ->  ps )
31, 2syl 16 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-12 1840
This theorem depends on definitions:  df-bi 185  df-ex 1600
This theorem is referenced by:  2sp  1852  19.2g  1854  axc112  1923  ax12v2  2069  equveli  2074  dfsb2  2100  drsb1  2104  drsb2  2105  nfsb4t  2116  sbi1  2119  sbco2  2144  sbco3  2146  sb9  2155  sbal1  2190  eujustALT  2271  mo3OLD  2310  2eu6  2369  ralcom2  3008  ceqsalgALT  3121  reu6  3274  sbcal  3365  reldisj  3856  dfnfc2  4252  eusvnfb  4633  nfnid  4666  mosubopt  4735  dfid3  4786  issref  5370  fv3  5869  fvmptt  5956  fnoprabg  6388  pssnn  7740  kmlem16  8548  nd3  8967  axunndlem1  8973  axunnd  8974  axpowndlem1  8975  axpowndlem3OLD  8979  axregndlem1  8982  axregndlem2  8983  axregndOLD  8985  axacndlem5  8992  bwthOLD  19784  fundmpss  29171  wfrlem5  29322  frrlem5  29366  nalf  29843  unisym1  29863  wl-nfimf1  29953  wl-dral1d  29959  wl-nfs1t  29966  wl-sb8t  29975  wl-sbhbt  29977  wl-equsb4  29980  wl-sbalnae  29987  wl-mo3t  29996  wl-ax11-lem5  30004  wl-ax11-lem8  30007  wl-sbcom3  30010  pm11.57  31249  axc5c4c711toc7  31265  axc11next  31267  pm14.122b  31284  dropab1  31310  dropab2  31311  ax6e2eq  33063  bj-axc15v  34078
  Copyright terms: Public domain W3C validator