Metamath Proof Explorer

Theorem ccat2s1fstOLD

Description: Obsolete version of ccat2s1fst as of 28-Jan-2024. The first symbol of the concatenation of a word with two single symbols. (Contributed by Alexander van der Vekens, 22-Sep-2018) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

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