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

Theorem sps 1412
Description: Generalization of antecedent. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
sps.1 (φψ)
Assertion
Ref Expression
sps (xφψ)

Proof of Theorem sps
StepHypRef Expression
1 sp 1382 . 2 (xφφ)
2 sps.1 . 2 (φψ)
31, 2syl 14 1 (xφψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1226
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-4 1381
This theorem is referenced by:  19.21ht  1455  exim  1472  alexdc  1492  19.2  1511  ax10o  1585  hbae  1588  cbv1h  1615  equvini  1623  equveli  1624  ax10oe  1660  drex1  1661  drsb1  1662  exdistrfor  1663  ax11v2  1683  equs5or  1693  sbequi  1702  drsb2  1704  spsbim  1706  sbcomxyyz  1828  hbsb4t  1871  mopick  1960  eupickbi  1964  ceqsalg  2559  mo2icl  2697  reu6  2707  sbcal  2787  csbie2t  2871  reldisj  3248  dfnfc2  3572  ssopab2  3986  eusvnfb  4136  mosubopt  4332  issref  4634  fv3  5122  fvmptt  5187  fnoprabg  5525  bj-exlimmp  7016  strcollnft  7202
  Copyright terms: Public domain W3C validator