Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > spsd | Structured version Visualization version GIF version |
Description: Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.) |
Ref | Expression |
---|---|
spsd.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
spsd | ⊢ (𝜑 → (∀𝑥𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sp 2041 | . 2 ⊢ (∀𝑥𝜓 → 𝜓) | |
2 | spsd.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | syl5 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 |