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 2172 | . 2 ⊢ (∀𝑥𝜑 → 𝜑) | |
2 | sps.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | syl 17 | 1 ⊢ (∀𝑥𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1526 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-ex 1772 |
This theorem is referenced by: 2sp 2175 19.2g 2177 nfim1 2190 axc16g 2252 drsb2 2258 axc11r 2379 axc15 2438 axc15OLD 2439 equvel 2474 sb1OLD 2503 sb4a 2505 dfsb1 2506 dfsb2 2528 drsb1 2531 nfsb4t 2535 sbi1OLD 2538 sbco2 2549 sbco3 2551 sb9 2557 sbal1 2568 sbal2 2569 dfsb2ALT 2587 nfsb4tALT 2600 sbi1ALT 2602 sbco2ALT 2611 eujustALT 2653 2eu6 2740 ralcom2 3364 ceqsalgALT 3531 reu6 3716 sbcal 3832 rexdifi 4121 reldisj 4400 dfnfc2 4850 nfnid 5268 eusvnfb 5285 mosubopt 5392 dfid3 5456 fv3 6682 fvmptt 6781 fnoprabg 7264 wfrlem5 7950 pssnn 8725 kmlem16 9580 nd3 10000 axunndlem1 10006 axunnd 10007 axpowndlem1 10008 axregndlem1 10013 axregndlem2 10014 axacndlem5 10022 fundmpss 32907 fprlem1 33035 frrlem15 33040 nalfal 33649 unisym1 33669 bj-sbsb 34058 bj-ax9 34114 wl-nfimf1 34649 wl-dral1d 34653 wl-nfs1t 34659 wl-sb8t 34670 wl-sbhbt 34672 wl-equsb4 34675 wl-sbalnae 34680 wl-2spsbbi 34683 wl-mo3t 34694 wl-ax11-lem5 34703 wl-ax11-lem8 34706 cotrintab 39854 pm11.57 40601 axc5c4c711toc7 40616 axc11next 40618 pm14.122b 40635 dropab1 40659 dropab2 40660 ax6e2eq 40771 |
Copyright terms: Public domain | W3C validator |