Metamath Proof Explorer

Theorem ccat2s1fst

Description: The first symbol of the concatenation of a word with two single symbols. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by AV, 28-Jan-2024)

Ref Expression
Assertion ccat2s1fst ⊢ W ∈ Word V ∧ 0 < W → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 = W ⁡ 0

Proof

Step Hyp Ref Expression
1 0nn0 ⊢ 0 ∈ ℕ 0
2 ccat2s1fvw ⊢ W ∈ Word V ∧ 0 ∈ ℕ 0 ∧ 0 < W → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 = W ⁡ 0
3 1 2 mp3an2 ⊢ W ∈ Word V ∧ 0 < W → W ++ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ ⁡ 0 = W ⁡ 0