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

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

Proof of Theorem sps
StepHypRef Expression
1 sp 1716 . 2  |-  ( A. x ph  ->  ph )
2 sps.1 . 2  |-  ( ph  ->  ps )
31, 2syl 15 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527
This theorem is referenced by:  19.2g  1780  ax10lem4  1881  ax10lem6  1883  ax10o  1892  cbv1h  1918  equveli  1928  ax11v2  1932  drsb1  1962  dfsb2  1995  sbequi  1999  drsb2  2001  sbn  2002  sbi1  2003  nfsb4t  2020  sbco2  2026  sbcom  2029  sbcom2  2053  sbal1  2065  eujustALT  2146  mopick  2205  eupickbi  2209  ralcom2  2704  ceqsalg  2812  reu6  2954  sbcal  3038  csbie2t  3125  reldisj  3498  dfnfc2  3845  nfnid  4204  mosubopt  4264  ssopab2  4290  dfid3  4310  eusvnfb  4530  issref  5056  fv3  5541  fvmptt  5615  fnoprabg  5945  pssnn  7081  kmlem16  7791  nd3  8211  axextnd  8213  axunndlem1  8217  axunnd  8218  axpowndlem1  8219  axpowndlem3  8221  axregndlem1  8224  axregndlem2  8225  axregnd  8226  axacndlem5  8233  fundmpss  24122  wfrlem5  24260  frrlem5  24285  nalf  24842  unisym1  24862  qusp  25542  bwt2  25592  imonclem  25813  pm11.57  27588  ax4567to6  27604  ax10ext  27606  pm14.122b  27623  pm14.123b  27626  dropab1  27650  dropab2  27651  a9e2eq  28323  ax12-2  29103  a12lem1  29130
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
  Copyright terms: Public domain W3C validator