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

Theorem sps 1473
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 1444 . 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 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-4 1443
This theorem is referenced by:  19.21ht  1516  exim  1533  alexdc  1553  19.2  1572  ax10o  1647  hbae  1650  cbv1h  1677  equvini  1685  equveli  1686  ax10oe  1722  drex1  1723  drsb1  1724  exdistrfor  1725  ax11v2  1745  equs5or  1755  sbequi  1764  drsb2  1766  spsbim  1768  sbcomxyyz  1891  hbsb4t  1934  mopick  2023  eupickbi  2027  ceqsalg  2641  mo2icl  2785  reu6  2795  sbcal  2879  csbie2t  2965  dfss4st  3221  reldisj  3322  dfnfc2  3654  ssopab2  4076  eusvnfb  4250  mosubopt  4471  issref  4781  fv3  5291  fvmptt  5357  fnoprabg  5703  bj-exlimmp  11115  strcollnft  11324
  Copyright terms: Public domain W3C validator