![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > s3cli | Structured version Visualization version GIF version |
Description: A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
Ref | Expression |
---|---|
s3cli | ⊢ 〈“𝐴𝐵𝐶”〉 ∈ Word V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-s3 13938 | . 2 ⊢ 〈“𝐴𝐵𝐶”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) | |
2 | s2cli 13969 | . 2 ⊢ 〈“𝐴𝐵”〉 ∈ Word V | |
3 | 1, 2 | cats1cli 13946 | 1 ⊢ 〈“𝐴𝐵𝐶”〉 ∈ Word V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2157 Vcvv 3389 Word cword 13538 〈“cs2 13930 〈“cs3 13931 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2379 ax-ext 2781 ax-rep 4968 ax-sep 4979 ax-nul 4987 ax-pow 5039 ax-pr 5101 ax-un 7187 ax-cnex 10284 ax-resscn 10285 ax-1cn 10286 ax-icn 10287 ax-addcl 10288 ax-addrcl 10289 ax-mulcl 10290 ax-mulrcl 10291 ax-mulcom 10292 ax-addass 10293 ax-mulass 10294 ax-distr 10295 ax-i2m1 10296 ax-1ne0 10297 ax-1rid 10298 ax-rnegex 10299 ax-rrecex 10300 ax-cnre 10301 ax-pre-lttri 10302 ax-pre-lttrn 10303 ax-pre-ltadd 10304 ax-pre-mulgt0 10305 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2593 df-eu 2611 df-clab 2790 df-cleq 2796 df-clel 2799 df-nfc 2934 df-ne 2976 df-nel 3079 df-ral 3098 df-rex 3099 df-reu 3100 df-rab 3102 df-v 3391 df-sbc 3638 df-csb 3733 df-dif 3776 df-un 3778 df-in 3780 df-ss 3787 df-pss 3789 df-nul 4120 df-if 4282 df-pw 4355 df-sn 4373 df-pr 4375 df-tp 4377 df-op 4379 df-uni 4633 df-int 4672 df-iun 4716 df-br 4848 df-opab 4910 df-mpt 4927 df-tr 4950 df-id 5224 df-eprel 5229 df-po 5237 df-so 5238 df-fr 5275 df-we 5277 df-xp 5322 df-rel 5323 df-cnv 5324 df-co 5325 df-dm 5326 df-rn 5327 df-res 5328 df-ima 5329 df-pred 5902 df-ord 5948 df-on 5949 df-lim 5950 df-suc 5951 df-iota 6068 df-fun 6107 df-fn 6108 df-f 6109 df-f1 6110 df-fo 6111 df-f1o 6112 df-fv 6113 df-riota 6843 df-ov 6885 df-oprab 6886 df-mpt2 6887 df-om 7304 df-1st 7405 df-2nd 7406 df-wrecs 7649 df-recs 7711 df-rdg 7749 df-1o 7803 df-oadd 7807 df-er 7986 df-en 8200 df-dom 8201 df-sdom 8202 df-fin 8203 df-card 9055 df-pnf 10369 df-mnf 10370 df-xr 10371 df-ltxr 10372 df-le 10373 df-sub 10562 df-neg 10563 df-nn 11317 df-n0 11585 df-z 11671 df-uz 11935 df-fz 12585 df-fzo 12725 df-hash 13375 df-word 13539 df-concat 13595 df-s1 13620 df-s2 13937 df-s3 13938 |
This theorem is referenced by: s4cli 13971 s4fv0 13984 s4fv1 13985 s4fv2 13986 s4fv3 13987 s4len 13988 lsws3 13994 s1s4 14014 s4s4 14021 s3s4 14022 s3sndisj 14053 s3iunsndisj 14054 uncfval 17193 2wlkd 27229 2wlkond 27230 2trlond 27232 2pthd 27233 2pthond 27235 umgr2adedgwlkonALT 27240 umgr2wlk 27242 elwwlks2 27261 elwspths2spth 27262 3wlkd 27518 3trlond 27521 3pthond 27523 3spthond 27525 uhgr3cyclex 27530 konigsberglem1 27603 konigsberglem2 27604 konigsberglem3 27605 fusgreghash2wspv 27688 |
Copyright terms: Public domain | W3C validator |