This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem s3cld

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

Ref Expression
Hypotheses s2cld.1 ⊢ φ → A ∈ X
s2cld.2 ⊢ φ → B ∈ X
s3cld.3 ⊢ φ → C ∈ X
Assertion s3cld ⊢ φ → ⟨“ ABC ”⟩ ∈ Word X

Proof

Step Hyp Ref Expression
1 s2cld.1 ⊢ φ → A ∈ X
2 s2cld.2 ⊢ φ → B ∈ X
3 s3cld.3 ⊢ φ → C ∈ X
4 df-s3 ⊢ ⟨“ ABC ”⟩ = ⟨“ AB ”⟩ ++ ⟨“ C ”⟩
5 1 2 s2cld ⊢ φ → ⟨“ AB ”⟩ ∈ Word X
6 4 5 3 cats1cld ⊢ φ → ⟨“ ABC ”⟩ ∈ Word X