ccatw2s1ccatws2

Description: The concatenation of a word with two singleton words equals the concatenation of the word with the doubleton word consisting of the symbols of the two singletons. (Contributed by Mario Carneiro/AV, 21-Oct-2018) (Revised by AV, 29-Jan-2024)

		Ref	Expression
	Assertion	ccatw2s1ccatws2	$⊢ W \in Word V \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = W ++ ⟨“ X Y ”⟩$

Proof

Step	Hyp	Ref	Expression
1		ccatw2s1ass	$⊢ W \in Word V \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)$
2		df-s2	$⊢ ⟨“ X Y ”⟩ = ⟨“ X ”⟩ ++ ⟨“ Y ”⟩$
3	2	eqcomi	$⊢ ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = ⟨“ X Y ”⟩$
4	3	a1i	$⊢ W \in Word V \to ⟨“ X ”⟩ ++ ⟨“ Y ”⟩ = ⟨“ X Y ”⟩$
5	4	oveq2d	$⊢ W \in Word V \to W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩) = W ++ ⟨“ X Y ”⟩$
6	1 5	eqtrd	$⊢ W \in Word V \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = W ++ ⟨“ X Y ”⟩$

Metamath Proof Explorer

Theorem ccatw2s1ccatws2

Proof