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

Theorem sps 1446
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 1417 . 2 (∀𝑥𝜑𝜑)
2 sps.1 . 2 (𝜑𝜓)
31, 2syl 14 1 (∀𝑥𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-4 1416
This theorem is referenced by:  19.21ht  1489  exim  1506  alexdc  1526  19.2  1545  ax10o  1619  hbae  1622  cbv1h  1649  equvini  1657  equveli  1658  ax10oe  1694  drex1  1695  drsb1  1696  exdistrfor  1697  ax11v2  1717  equs5or  1727  sbequi  1736  drsb2  1738  spsbim  1740  sbcomxyyz  1862  hbsb4t  1905  mopick  1994  eupickbi  1998  ceqsalg  2599  mo2icl  2743  reu6  2753  sbcal  2837  csbie2t  2922  reldisj  3299  dfnfc2  3626  ssopab2  4040  eusvnfb  4214  mosubopt  4433  issref  4735  fv3  5225  fvmptt  5290  fnoprabg  5630  bj-exlimmp  10296  strcollnft  10496
  Copyright terms: Public domain W3C validator