MPE Home 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