Metamath Proof Explorer

Theorem s3cl

Description: A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s3cl ⊢A∈X∧B∈X∧C∈X→⟨“ABC”⟩∈WordX

Proof

Step Hyp Ref Expression
1 simp1 ⊢A∈X∧B∈X∧C∈X→A∈X
2 simp2 ⊢A∈X∧B∈X∧C∈X→B∈X
3 simp3 ⊢A∈X∧B∈X∧C∈X→C∈X
4 1 2 3 s3cld ⊢A∈X∧B∈X∧C∈X→⟨“ABC”⟩∈WordX