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

Metamath Proof Explorer

Theorem s4cld

Description: A length 4 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
s4cld.4 ⊢ φ → D ∈ X
Assertion s4cld ⊢ φ → ⟨“ ABCD ”⟩ ∈ Word X

Proof

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