![]() |
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 2200 | . 2 ⊢ (∀𝑥𝜑 → 𝜑) | |
2 | sps.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | syl 17 | 1 ⊢ (∀𝑥𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1630 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-12 2196 |
This theorem depends on definitions: df-bi 197 df-ex 1854 |
This theorem is referenced by: 2sp 2203 19.2g 2205 nfim1 2214 axc16g 2281 axc11rvOLD 2287 axc11r 2332 axc15 2448 equvel 2484 dfsb2 2510 drsb1 2514 drsb2 2515 nfsb4t 2526 sbi1 2529 sbco2 2552 sbco3 2554 sb9 2563 sbal1 2597 eujustALT 2610 2eu6 2696 ralcom2 3242 ceqsalgALT 3371 reu6 3536 sbcal 3626 reldisj 4163 dfnfc2 4606 dfnfc2OLD 4607 eusvnfb 5011 nfnid 5046 mosubopt 5120 dfid3 5175 issref 5667 fv3 6367 fvmptt 6462 fnoprabg 6926 wfrlem5 7588 pssnn 8343 kmlem16 9179 nd3 9603 axunndlem1 9609 axunnd 9610 axpowndlem1 9611 axregndlem1 9616 axregndlem2 9617 axacndlem5 9625 fundmpss 31971 frrlem5 32090 nalf 32708 unisym1 32728 bj-sbsb 33130 bj-mo3OLD 33138 bj-ax9 33196 wl-nfimf1 33626 wl-dral1d 33631 wl-nfs1t 33637 wl-sb8t 33646 wl-sbhbt 33648 wl-equsb4 33651 wl-sbalnae 33658 wl-mo3t 33671 wl-ax11-lem5 33679 wl-ax11-lem8 33682 wl-sbcom3 33685 cotrintab 38423 pm11.57 39091 axc5c4c711toc7 39107 axc11next 39109 pm14.122b 39126 dropab1 39153 dropab2 39154 ax6e2eq 39275 |
Copyright terms: Public domain | W3C validator |