ccatw2s1ccatws2OLD

Description: Obsolete version of ccatw2s1ccatws2 as of 29-Jan-2024. 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) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

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

Metamath Proof Explorer

Theorem ccatw2s1ccatws2OLD

Proof