ccatw2s1assOLD

Description: Obsolete version of ccatw2s1ass as of 29-Jan-2024. Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	ccatw2s1assOLD	$⊢ (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		id	$⊢ W \in Word V \to W \in Word V$
2		s1cl	$⊢ X \in V \to ⟨“ X ”⟩ \in Word V$
3		s1cl	$⊢ Y \in V \to ⟨“ Y ”⟩ \in Word V$
4		ccatass	$⊢ (W \in Word V \land ⟨“ X ”⟩ \in Word V \land ⟨“ Y ”⟩ \in Word V) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)$
5	1 2 3 4	syl3an	$⊢ (W \in Word V \land X \in V \land Y \in V) \to (W ++ ⟨“ X ”⟩) ++ ⟨“ Y ”⟩ = W ++ (⟨“ X ”⟩ ++ ⟨“ Y ”⟩)$

Metamath Proof Explorer

Theorem ccatw2s1assOLD

Proof