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

Theorem spsd 2045
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 2041 . 2 (∀𝑥𝜓𝜓)
2 spsd.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5 33 1 (𝜑 → (∀𝑥𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034
This theorem depends on definitions:  df-bi 196  df-ex 1696
This theorem is referenced by:  axc11v  2123  axc11rv  2124  axc11rvOLD  2125  axc11nlemOLD  2146  axc11nlemALT  2294  equvel  2335  nfsb4t  2377  mo2v  2465  moexex  2529  2eu6  2546  zorn2lem4  9204  zorn2lem5  9205  axpowndlem3  9300  axacndlem5  9312  axc11n11r  31860  wl-equsal1i  32508  axc5c4c711  37624
  Copyright terms: Public domain W3C validator