MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  spsd Structured version   Unicode version

Theorem spsd 1771
Description: Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.)
Hypothesis
Ref Expression
spsd.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
spsd  |-  ( ph  ->  ( A. x ps 
->  ch ) )

Proof of Theorem spsd
StepHypRef Expression
1 sp 1763 . 2  |-  ( A. x ps  ->  ps )
2 spsd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 30 1  |-  ( ph  ->  ( A. x ps 
->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549
This theorem is referenced by:  ax10lem2  2023  ax10lem4OLD  2030  nfsb4t  2127  moexex  2350  zorn2lem4  8379  zorn2lem5  8380  axpowndlem3  8474  axacndlem5  8486  ax4567  27578  cbv3hvNEW7  29446  ax10lem4NEW7  29471  ax7w2AUX7  29650  ax7w7tAUX7  29656
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator