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

Theorem spsd 2055
 Description: Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.)
Hypothesis
Ref Expression
spsd.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
spsd (𝜑 → (∀𝑥𝜓𝜒))

Proof of Theorem spsd
StepHypRef Expression
1 sp 2051 . 2 (∀𝑥𝜓𝜓)
2 spsd.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 34 1 (𝜑 → (∀𝑥𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1479 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-12 2045 This theorem depends on definitions:  df-bi 197  df-ex 1703 This theorem is referenced by:  axc11v  2136  axc11rv  2137  axc11rvOLD  2138  axc11nlemOLD  2158  axc11nlemALT  2304  equvel  2345  nfsb4t  2387  mo2v  2475  moexex  2539  2eu6  2556  zorn2lem4  9306  zorn2lem5  9307  axpowndlem3  9406  axacndlem5  9418  axc11n11r  32648  wl-equsal1i  33300  axc5c4c711  38422
 Copyright terms: Public domain W3C validator