![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sstri | GIF version |
Description: Subclass transitivity inference. (Contributed by NM, 5-May-2000.) |
Ref | Expression |
---|---|
sstri.1 | ⊢ 𝐴 ⊆ 𝐵 |
sstri.2 | ⊢ 𝐵 ⊆ 𝐶 |
Ref | Expression |
---|---|
sstri | ⊢ 𝐴 ⊆ 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstri.1 | . 2 ⊢ 𝐴 ⊆ 𝐵 | |
2 | sstri.2 | . 2 ⊢ 𝐵 ⊆ 𝐶 | |
3 | sstr2 3176 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) | |
4 | 1, 2, 3 | mp2 16 | 1 ⊢ 𝐴 ⊆ 𝐶 |
Colors of variables: wff set class |
Syntax hints: ⊆ wss 3143 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-11 1516 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2170 |
This theorem depends on definitions: df-bi 117 df-nf 1471 df-sb 1773 df-clab 2175 df-cleq 2181 df-clel 2184 df-in 3149 df-ss 3156 |
This theorem is referenced by: difdif2ss 3406 difdifdirss 3521 snsstp1 3756 snsstp2 3757 nnregexmid 4634 dmexg 4905 rnexg 4906 ssrnres 5085 cossxp 5165 cocnvss 5168 funinsn 5279 fabexg 5417 foimacnv 5493 ssimaex 5592 oprabss 5976 tposssxp 6267 mapsspw 6701 sbthlemi5 6977 sbthlem7 6979 caserel 7103 dmaddpi 7341 dmmulpi 7342 ltrelxr 8035 nnsscn 8941 nn0sscn 9198 nn0ssq 9645 nnssq 9646 qsscn 9648 fzval2 10028 fzossnn 10206 fzo0ssnn0 10232 expcl2lemap 10549 rpexpcl 10556 expge0 10573 expge1 10574 seq3coll 10839 summodclem2a 11406 fsum3cvg3 11421 fsumrpcl 11429 fsumge0 11484 prodmodclem2a 11601 fprodrpcl 11636 fprodge0 11662 fprodge1 11664 infssuzcldc 11969 isprm3 12135 eulerthlemrprm 12246 eulerthlema 12247 eulerthlemh 12248 eulerthlemth 12249 pcprecl 12306 pcprendvds 12307 pcpremul 12310 structfn 12498 strleun 12581 cnfldbas 13828 cnfldadd 13829 cnfldmul 13830 toponsspwpwg 13905 dmtopon 13906 lmbrf 14098 lmres 14131 txcnmpt 14156 qtopbas 14405 tgqioo 14430 dvrecap 14560 cosz12 14584 ioocosf1o 14658 lgsfcl2 14790 2sqlem6 14850 2sqlem8 14853 2sqlem9 14854 |
Copyright terms: Public domain | W3C validator |