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

Theorem sps 1427
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 1398 . 2 (xφφ)
2 sps.1 . 2 (φψ)
31, 2syl 14 1 (xφψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1240
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-4 1397
This theorem is referenced by:  19.21ht  1470  exim  1487  alexdc  1507  19.2  1526  ax10o  1600  hbae  1603  cbv1h  1630  equvini  1638  equveli  1639  ax10oe  1675  drex1  1676  drsb1  1677  exdistrfor  1678  ax11v2  1698  equs5or  1708  sbequi  1717  drsb2  1719  spsbim  1721  sbcomxyyz  1843  hbsb4t  1886  mopick  1975  eupickbi  1979  ceqsalg  2576  mo2icl  2714  reu6  2724  sbcal  2804  csbie2t  2888  reldisj  3265  dfnfc2  3589  ssopab2  4003  eusvnfb  4152  mosubopt  4348  issref  4650  fv3  5140  fvmptt  5205  fnoprabg  5544  bj-exlimmp  9178  strcollnft  9368
  Copyright terms: Public domain W3C validator