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

Theorem sps 1770
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 1763 . 2  |-  ( A. x ph  ->  ph )
2 sps.1 . 2  |-  ( ph  ->  ps )
31, 2syl 16 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549
This theorem is referenced by:  19.2g  1773  cbv1h  1974  cbv1hOLD  1975  ax10o2  2024  ax10lem4OLD  2030  ax9OLD  2033  ax10oOLD  2039  ax11v2  2078  ax11v2OLD  2079  equveliOLD  2086  dfsb2  2108  sbequi  2110  drsb1  2112  drsb2  2113  sbequiOLD  2114  nfsb4t  2127  nfsb4tOLD  2128  sbnOLD  2131  sbi1  2132  sbco2  2161  sbcom  2164  sbcomOLD  2165  sbcom2  2190  sbal1  2203  eujustALT  2284  mopick  2343  eupickbi  2347  ralcom2  2872  ceqsalg  2980  reu6  3123  sbcal  3208  csbie2t  3295  reldisj  3671  dfnfc2  4033  nfnid  4393  mosubopt  4454  ssopab2  4480  dfid3  4499  eusvnfb  4719  issref  5247  fv3  5744  fvmptt  5820  fnoprabg  6171  pssnn  7327  kmlem16  8045  nd3  8464  axextnd  8466  axunndlem1  8470  axunnd  8471  axpowndlem1  8472  axpowndlem3  8474  axregndlem1  8477  axregndlem2  8478  axregnd  8479  axacndlem5  8486  bwth  17473  fundmpss  25390  wfrlem5  25542  frrlem5  25586  nalf  26153  unisym1  26173  mbfresfi  26253  pm11.57  27565  ax4567to6  27581  ax10ext  27583  pm14.122b  27600  pm14.123b  27603  dropab1  27626  dropab2  27627  a9e2eq  28644  ax9NEW7  29468  ax10lem4NEW7  29471  ax10oNEW7  29476  drsb1NEW7  29506  cbv1hwAUX7  29511  equveliNEW7  29528  ax11v2NEW7  29530  sbnNEW7  29562  sbi1NEW7  29563  nfsb4twAUX7  29576  sbequiNEW7  29579  drsb2NEW7  29581  sbco2wAUX7  29585  sbcomwAUX7  29588  sbal1NEW7  29615  dfsb2NEW7  29638  sbcom2NEW7  29644  ax7w3AUX7  29651  ax7w8AUX7  29654  ax7w9AUX7  29660  ax7w16AUX7  29674  cbv1hOLD7  29719  nfsb4tOLD7  29745  nfsb4tw2AUXOLD7  29746  sbco2OLD7  29752  sbcomOLD7  29755
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator