![]() |
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 3033 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶)) | |
4 | 1, 2, 3 | mp2 16 | 1 ⊢ 𝐴 ⊆ 𝐶 |
Colors of variables: wff set class |
Syntax hints: ⊆ wss 3000 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-11 1443 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-in 3006 df-ss 3013 |
This theorem is referenced by: difdif2ss 3257 difdifdirss 3371 snsstp1 3593 snsstp2 3594 nnregexmid 4447 dmexg 4710 rnexg 4711 ssrnres 4886 cossxp 4966 cocnvss 4969 funinsn 5076 fabexg 5211 foimacnv 5284 ssimaex 5378 oprabss 5748 tposssxp 6028 mapsspw 6455 sbthlemi5 6724 sbthlem7 6726 djuin 6810 caserel 6832 dmaddpi 6945 dmmulpi 6946 ltrelxr 7608 nnsscn 8488 nn0sscn 8739 nn0ssq 9174 nnssq 9175 qsscn 9177 fzval2 9488 fzossnn 9661 fzo0ssnn0 9687 expcl2lemap 10028 rpexpcl 10035 expge0 10052 expge1 10053 iseqcoll 10308 isummolem2a 10832 fsum3cvg3 10850 fsumrpcl 10859 fsumge0 10914 infssuzcldc 11286 isprm3 11439 structfn 11574 strleun 11644 toponsspwpwg 11781 dmtopon 11782 |
Copyright terms: Public domain | W3C validator |