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

Theorem sps 1471
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 1442 . 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 1283
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-4 1441
This theorem is referenced by:  19.21ht  1514  exim  1531  alexdc  1551  19.2  1570  ax10o  1644  hbae  1647  cbv1h  1674  equvini  1682  equveli  1683  ax10oe  1719  drex1  1720  drsb1  1721  exdistrfor  1722  ax11v2  1742  equs5or  1752  sbequi  1761  drsb2  1763  spsbim  1765  sbcomxyyz  1888  hbsb4t  1931  mopick  2020  eupickbi  2024  ceqsalg  2628  mo2icl  2772  reu6  2782  sbcal  2866  csbie2t  2951  reldisj  3302  dfnfc2  3627  ssopab2  4038  eusvnfb  4212  mosubopt  4431  issref  4737  fv3  5229  fvmptt  5294  fnoprabg  5633  bj-exlimmp  10731  strcollnft  10937
  Copyright terms: Public domain W3C validator