![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sps | Structured version Visualization version Unicode version |
Description: Generalization of antecedent. (Contributed by NM, 5-Jan-1993.) |
Ref | Expression |
---|---|
sps.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sps |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sp 1937 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sps.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 17 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-12 1933 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 |
This theorem is referenced by: 2sp 1944 19.2g 1946 axc112 2020 ax12v2 2175 equveli 2180 dfsb2 2202 drsb1 2206 drsb2 2207 nfsb4t 2218 sbi1 2221 sbco2 2244 sbco3 2246 sb9 2255 sbal1 2289 eujustALT 2302 2eu6 2387 ralcom2 2955 ceqsalgALT 3073 reu6 3227 sbcal 3317 reldisj 3808 dfnfc2 4216 eusvnfb 4599 nfnid 4629 mosubopt 4699 dfid3 4750 issref 5213 fv3 5878 fvmptt 5965 fnoprabg 6397 wfrlem5 7040 pssnn 7790 kmlem16 8595 nd3 9014 axunndlem1 9020 axunnd 9021 axpowndlem1 9022 axregndlem1 9027 axregndlem2 9028 axacndlem5 9036 fundmpss 30407 frrlem5 30518 nalf 31063 unisym1 31083 bj-axc15v 31362 bj-mo3OLD 31447 wl-nfimf1 31858 wl-dral1d 31864 wl-nfs1t 31871 wl-sb8t 31880 wl-sbhbt 31882 wl-equsb4 31885 wl-sbalnae 31892 wl-mo3t 31905 wl-ax12v3 31912 wl-ax11-lem5 31919 wl-ax11-lem8 31922 wl-sbcom3 31925 cotrintab 36221 pm11.57 36739 axc5c4c711toc7 36755 axc11next 36757 pm14.122b 36774 dropab1 36800 dropab2 36801 ax6e2eq 36924 |
Copyright terms: Public domain | W3C validator |