![]() |
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 2177 | . 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 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-12 2172 |
This theorem depends on definitions: df-bi 206 df-ex 1783 |
This theorem is referenced by: 2sp 2180 19.2g 2182 nfim1 2193 axc16g 2252 drsb2 2258 axc11r 2366 axc15 2422 equvel 2456 sb4a 2480 dfsb1 2481 dfsb2 2493 drsb1 2495 nfsb4t 2499 sbco2 2511 sbco3 2513 sb9 2519 sbal1 2528 sbal2 2529 eujustALT 2567 2eu6 2653 ralcom2 3374 ceqsalgALT 3508 reu6 3721 sbcal 3840 rexdifi 4144 reldisjOLD 4451 dfnfc2 4932 nfnid 5372 eusvnfb 5390 mosubopt 5509 dfid3 5576 fv3 6906 fvmptt 7014 fnoprabg 7526 fprlem1 8280 wfrlem5OLD 8308 pssnn 9164 pssnnOLD 9261 frrlem15 9748 kmlem16 10156 nd3 10580 axunndlem1 10586 axunnd 10587 axpowndlem1 10588 axregndlem1 10593 axregndlem2 10594 axacndlem5 10602 fundmpss 34676 nalfal 35226 unisym1 35246 bj-sbsb 35653 wl-nfimf1 36333 wl-axc11r 36337 wl-dral1d 36338 wl-nfs1t 36344 wl-sb8t 36355 wl-sbhbt 36357 wl-equsb4 36360 wl-sbalnae 36365 wl-2spsbbi 36368 wl-mo3t 36379 wl-ax11-lem5 36389 wl-ax11-lem8 36392 cotrintab 42298 pm11.57 43081 axc5c4c711toc7 43096 axc11next 43098 pm14.122b 43115 dropab1 43139 dropab2 43140 ax6e2eq 43251 |
Copyright terms: Public domain | W3C validator |