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

Theorem sps 1751
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 1728 . 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 1530
This theorem is referenced by:  19.2g  1792  ax10lem4  1894  ax10lem6  1896  ax10o  1905  cbv1h  1931  equveli  1941  ax11v2  1945  drsb1  1975  dfsb2  2008  sbequi  2012  drsb2  2014  sbn  2015  sbi1  2016  nfsb4t  2033  sbco2  2039  sbcom  2042  sbcom2  2066  sbal1  2078  eujustALT  2159  mopick  2218  eupickbi  2222  ralcom2  2717  ceqsalg  2825  reu6  2967  sbcal  3051  csbie2t  3138  reldisj  3511  dfnfc2  3861  nfnid  4220  mosubopt  4280  ssopab2  4306  dfid3  4326  eusvnfb  4546  issref  5072  fv3  5557  fvmptt  5631  fnoprabg  5961  pssnn  7097  kmlem16  7807  nd3  8227  axextnd  8229  axunndlem1  8233  axunnd  8234  axpowndlem1  8235  axpowndlem3  8237  axregndlem1  8240  axregndlem2  8241  axregnd  8242  axacndlem5  8249  fundmpss  24193  wfrlem5  24331  frrlem5  24356  nalf  24914  unisym1  24934  qusp  25645  bwt2  25695  imonclem  25916  pm11.57  27691  ax4567to6  27707  ax10ext  27709  pm14.122b  27726  pm14.123b  27729  dropab1  27753  dropab2  27754  a9e2eq  28622  ax10lem4NEW7  29448  ax10oNEW7  29453  drsb1NEW7  29483  cbv1hwAUX7  29488  equveliNEW7  29503  ax11v2NEW7  29505  sbnNEW7  29537  sbi1NEW7  29538  nfsb4twAUX7  29551  sbequiNEW7  29553  drsb2NEW7  29555  sbco2wAUX7  29559  sbcomwAUX7  29562  sbal1NEW7  29587  dfsb2NEW7  29609  ax7w8AUX7  29624  ax7w9AUX7  29630  cbv1hOLD7  29673  nfsb4tOLD7  29699  nfsb4tw2AUXOLD7  29700  sbco2OLD7  29706  sbcomOLD7  29709  sbcom2OLD7  29715  ax12-2  29725  a12lem1  29752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
  Copyright terms: Public domain W3C validator