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

Theorem spsd 1816
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 1808 . 2  |-  ( A. x ps  ->  ps )
2 spsd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5 32 1  |-  ( ph  ->  ( A. x ps 
->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  axc11nlem  1885  axc11nlemOLD  2021  equveli  2061  nfsb4t  2103  mo2v  2282  mo2vOLD  2283  mo2vOLDOLD  2284  moexex  2371  moexexOLD  2372  2eu6  2393  zorn2lem4  8880  zorn2lem5  8881  axpowndlem3  8976  axpowndlem3OLD  8977  axacndlem5  8990  wl-equsal1i  29849  axc5c4c711  31113  bj-axc11nlemv  33613
  Copyright terms: Public domain W3C validator