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 ”⟩ ∈ Word X

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 ”⟩ ∈ Word X