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 2182 | . 2 ⊢ (∀𝑥𝜑 → 𝜑) | |
2 | sps.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | syl 17 | 1 ⊢ (∀𝑥𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1535 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-12 2177 |
This theorem depends on definitions: df-bi 209 df-ex 1781 |
This theorem is referenced by: 2sp 2185 19.2g 2187 nfim1 2199 axc16g 2261 drsb2 2267 axc11r 2386 axc15 2444 equvel 2479 sb1OLD 2507 sb4a 2509 dfsb1 2510 dfsb2 2532 drsb1 2535 nfsb4t 2539 sbi1OLD 2542 sbco2 2553 sbco3 2555 sb9 2561 sbal1 2572 sbal2 2573 dfsb2ALT 2591 nfsb4tALT 2604 sbi1ALT 2606 sbco2ALT 2615 eujustALT 2657 2eu6 2742 ralcom2 3365 ceqsalgALT 3532 reu6 3719 sbcal 3835 rexdifi 4124 reldisj 4404 dfnfc2 4862 nfnid 5278 eusvnfb 5296 mosubopt 5402 dfid3 5464 fv3 6690 fvmptt 6790 fnoprabg 7277 wfrlem5 7961 pssnn 8738 kmlem16 9593 nd3 10013 axunndlem1 10019 axunnd 10020 axpowndlem1 10021 axregndlem1 10026 axregndlem2 10027 axacndlem5 10035 fundmpss 33011 fprlem1 33139 frrlem15 33144 nalfal 33753 unisym1 33773 bj-sbsb 34162 bj-ax9 34218 wl-nfimf1 34768 wl-axc11r 34772 wl-dral1d 34773 wl-nfs1t 34779 wl-sb8t 34790 wl-sbhbt 34792 wl-equsb4 34795 wl-sbalnae 34800 wl-2spsbbi 34803 wl-mo3t 34814 wl-ax11-lem5 34823 wl-ax11-lem8 34826 cotrintab 39981 pm11.57 40728 axc5c4c711toc7 40743 axc11next 40745 pm14.122b 40762 dropab1 40786 dropab2 40787 ax6e2eq 40898 |
Copyright terms: Public domain | W3C validator |