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 2176 | . 2 ⊢ (∀𝑥𝜑 → 𝜑) | |
2 | sps.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | syl 17 | 1 ⊢ (∀𝑥𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1537 |
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 1913 ax-6 1971 ax-7 2011 ax-12 2171 |
This theorem depends on definitions: df-bi 206 df-ex 1783 |
This theorem is referenced by: 2sp 2179 19.2g 2181 nfim1 2192 axc16g 2252 drsb2 2258 axc11r 2366 axc15 2422 equvel 2456 sb1OLD 2482 sb4a 2484 dfsb1 2485 dfsb2 2497 drsb1 2499 nfsb4t 2503 sbco2 2515 sbco3 2517 sb9 2523 sbal1 2533 sbal2 2534 eujustALT 2572 2eu6 2658 ralcom2 3290 ceqsalgALT 3465 reu6 3661 sbcal 3780 rexdifi 4080 reldisjOLD 4386 dfnfc2 4863 nfnid 5298 eusvnfb 5316 mosubopt 5424 dfid3 5492 fv3 6792 fvmptt 6895 fnoprabg 7397 fprlem1 8116 wfrlem5OLD 8144 pssnn 8951 pssnnOLD 9040 frrlem15 9515 kmlem16 9921 nd3 10345 axunndlem1 10351 axunnd 10352 axpowndlem1 10353 axregndlem1 10358 axregndlem2 10359 axacndlem5 10367 fundmpss 33740 nalfal 34592 unisym1 34612 bj-sbsb 35020 wl-nfimf1 35685 wl-axc11r 35689 wl-dral1d 35690 wl-nfs1t 35696 wl-sb8t 35707 wl-sbhbt 35709 wl-equsb4 35712 wl-sbalnae 35717 wl-2spsbbi 35720 wl-mo3t 35731 wl-ax11-lem5 35740 wl-ax11-lem8 35743 cotrintab 41222 pm11.57 42007 axc5c4c711toc7 42022 axc11next 42024 pm14.122b 42041 dropab1 42065 dropab2 42066 ax6e2eq 42177 |
Copyright terms: Public domain | W3C validator |