ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sps Unicode version

Theorem sps 1500
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 1471 . 2  |-  ( A. x ph  ->  ph )
2 sps.1 . 2  |-  ( ph  ->  ps )
31, 2syl 14 1  |-  ( A. x ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1312
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 1470
This theorem is referenced by:  19.21ht  1543  exim  1561  alexdc  1581  19.2  1600  ax10o  1676  hbae  1679  cbv1h  1706  equvini  1714  equveli  1715  ax10oe  1751  drex1  1752  drsb1  1753  exdistrfor  1754  ax11v2  1774  equs5or  1784  sbequi  1793  drsb2  1795  spsbim  1797  sbcomxyyz  1921  hbsb4t  1964  mopick  2053  eupickbi  2057  ceqsalg  2686  mo2icl  2834  reu6  2844  sbcal  2930  csbie2t  3016  dfss4st  3277  reldisj  3382  dfnfc2  3722  ssopab2  4165  eusvnfb  4343  mosubopt  4572  issref  4889  fv3  5410  fvmptt  5478  fnoprabg  5838  bj-exlimmp  12810  strcollnft  13016
  Copyright terms: Public domain W3C validator