Theorem ccatidid

Description: Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022)

	Ref	Expression
Assertion	ccatidid	⊢ ( ∅ ++ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		wrd0	⊢ ∅ ∈ Word V
2		ccatlid	⊢ ( ∅ ∈ Word V → ( ∅ ++ ∅ ) = ∅ )
3	1 2	ax-mp	⊢ ( ∅ ++ ∅ ) = ∅