Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sstrdi | Unicode version |
Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
sstrdi.1 | |
sstrdi.2 |
Ref | Expression |
---|---|
sstrdi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstrdi.1 | . 2 | |
2 | sstrdi.2 | . . 3 | |
3 | 2 | a1i 9 | . 2 |
4 | 1, 3 | sstrd 3157 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wss 3121 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-11 1499 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-in 3127 df-ss 3134 |
This theorem is referenced by: difss2 3255 sstpr 3742 rintm 3963 eqbrrdva 4779 dmxpss2 5041 rnxpss2 5042 ssxpbm 5044 ssxp1 5045 ssxp2 5046 relfld 5137 funssxp 5365 dff2 5638 fliftf 5776 1stcof 6140 2ndcof 6141 tfrlemibfn 6305 tfr1onlembfn 6321 tfrcllemssrecs 6329 tfrcllembfn 6334 sucinc2 6423 peano5nnnn 7847 peano5nni 8874 suprzclex 9303 ioodisj 9943 fzssnn 10017 fzossnn0 10124 elfzom1elp1fzo 10151 frecuzrdgtcl 10361 frecuzrdgdomlem 10366 frecuzrdgfunlem 10368 zfz1iso 10769 seq3coll 10770 summodclem2a 11337 summodclem2 11338 zsumdc 11340 fsumsersdc 11351 fsum3cvg3 11352 prodmodclem2a 11532 prodmodclem2 11533 zproddc 11535 exmidunben 12374 nninfdclemp1 12398 strsetsid 12442 lmss 13005 dvbssntrcntop 13412 dvcjbr 13431 reeff1olem 13451 peano5set 13940 |
Copyright terms: Public domain | W3C validator |