![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sps | Unicode version |
Description: Generalization of antecedent. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sps.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sps |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sp 1398 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sps.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-4 1397 |
This theorem is referenced by: 19.21ht 1470 exim 1487 alexdc 1507 19.2 1526 ax10o 1600 hbae 1603 cbv1h 1630 equvini 1638 equveli 1639 ax10oe 1675 drex1 1676 drsb1 1677 exdistrfor 1678 ax11v2 1698 equs5or 1708 sbequi 1717 drsb2 1719 spsbim 1721 sbcomxyyz 1843 hbsb4t 1886 mopick 1975 eupickbi 1979 ceqsalg 2576 mo2icl 2714 reu6 2724 sbcal 2804 csbie2t 2888 reldisj 3265 dfnfc2 3589 ssopab2 4003 eusvnfb 4152 mosubopt 4348 issref 4650 fv3 5140 fvmptt 5205 fnoprabg 5544 bj-exlimmp 9244 strcollnft 9444 |
Copyright terms: Public domain | W3C validator |