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

Theorem sps 1473
Description: Generalization of antecedent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
sps.1 (𝜑𝜓)
Assertion
Ref Expression
sps (∀𝑥𝜑𝜓)

Proof of Theorem sps
StepHypRef Expression
1 sp 1444 . 2 (∀𝑥𝜑𝜑)
2 sps.1 . 2 (𝜑𝜓)
31, 2syl 14 1 (∀𝑥𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  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  3656  ssopab2  4078  eusvnfb  4252  mosubopt  4473  issref  4783  fv3  5293  fvmptt  5359  fnoprabg  5705  bj-exlimmp  11139  strcollnft  11348
  Copyright terms: Public domain W3C validator