| 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 1538 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-12 2177 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: 2sp 2186 19.2g 2188 nfim1 2199 axc16g 2260 drsb2 2266 axc11r 2371 axc15 2427 equvel 2461 sb4a 2485 dfsb1 2486 dfsb2 2498 drsb1 2500 nfsb4t 2504 sbco2 2516 sbco3 2518 sb9 2524 sbal1 2533 sbal2 2534 eujustALT 2572 2eu6 2657 ralcom2 3377 ceqsalgALT 3518 reu6 3732 sbcal 3849 rexdifi 4150 dfnfc2 4929 nfnid 5375 eusvnfb 5393 mosubopt 5515 dfid3 5581 fv3 6924 fvmptt 7036 fnoprabg 7556 fprlem1 8325 wfrlem5OLD 8353 pssnn 9208 frrlem15 9797 kmlem16 10206 nd3 10629 axunndlem1 10635 axunnd 10636 axpowndlem1 10637 axregndlem1 10642 axregndlem2 10643 axacndlem5 10651 axsepg2 35096 axsepg2ALT 35097 axnulg 35106 fundmpss 35767 nalfal 36404 unisym1 36424 bj-sbsb 36838 wl-nfimf1 37527 wl-axc11r 37531 wl-dral1d 37532 wl-nfs1t 37538 wl-sb8t 37553 wl-sbhbt 37555 wl-equsb4 37558 wl-sbalnae 37563 wl-2spsbbi 37566 wl-mo3t 37577 wl-ax11-lem5 37590 wl-ax11-lem8 37593 cotrintab 43627 pm11.57 44408 axc5c4c711toc7 44423 axc11next 44425 pm14.122b 44442 dropab1 44466 dropab2 44467 ax6e2eq 44577 |
| Copyright terms: Public domain | W3C validator |