Theorem s3cl

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

	Ref	Expression
Assertion	s3cl	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
2		simp2	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
3		simp3	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → 𝐶 ∈ 𝑋 )
4	1 2 3	s3cld	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ∈ Word 𝑋 )