Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sps | Structured version Visualization version GIF version |
Description: Generalization of antecedent. (Contributed by NM, 5-Jan-1993.) |
Ref | Expression |
---|---|
sps.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
sps | ⊢ (∀𝑥𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sp 2183 | . 2 ⊢ (∀𝑥𝜑 → 𝜑) | |
2 | sps.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | syl 17 | 1 ⊢ (∀𝑥𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-12 2178 |
This theorem depends on definitions: df-bi 210 df-ex 1787 |
This theorem is referenced by: 2sp 2186 19.2g 2188 nfim1 2200 axc16g 2260 drsb2 2266 axc11r 2367 axc15 2421 equvel 2455 sb1OLD 2482 sb4a 2484 dfsb1 2485 dfsb2 2497 drsb1 2499 nfsb4t 2503 sbco2 2515 sbco3 2517 sb9 2523 sbal1 2533 sbal2 2534 eujustALT 2573 2eu6 2659 ralcom2 3265 ceqsalgALT 3430 reu6 3623 sbcal 3740 rexdifi 4034 reldisjOLD 4339 dfnfc2 4817 nfnid 5239 eusvnfb 5257 mosubopt 5364 dfid3 5427 fv3 6686 fvmptt 6789 fnoprabg 7283 wfrlem5 7981 pssnn 8760 pssnnOLD 8808 kmlem16 9658 nd3 10082 axunndlem1 10088 axunnd 10089 axpowndlem1 10090 axregndlem1 10095 axregndlem2 10096 axacndlem5 10104 fundmpss 33304 fprlem1 33447 frrlem15 33452 nalfal 34222 unisym1 34242 bj-sbsb 34640 wl-nfimf1 35297 wl-axc11r 35301 wl-dral1d 35302 wl-nfs1t 35308 wl-sb8t 35319 wl-sbhbt 35321 wl-equsb4 35324 wl-sbalnae 35329 wl-2spsbbi 35332 wl-mo3t 35343 wl-ax11-lem5 35352 wl-ax11-lem8 35355 cotrintab 40751 pm11.57 41529 axc5c4c711toc7 41544 axc11next 41546 pm14.122b 41563 dropab1 41587 dropab2 41588 ax6e2eq 41699 |
Copyright terms: Public domain | W3C validator |