Theorem ccatidid

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

	Ref	Expression
Assertion	ccatidid	$$⊢\varnothing \mathrm{++}\varnothing =\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		wrd0	$$⊢\varnothing \in \mathrm{Word}\mathrm{V}$$
2		ccatlid	$$⊢\varnothing \in \mathrm{Word}\mathrm{V}\to \varnothing \mathrm{++}\varnothing =\varnothing$$
3	1 2	ax-mp	$$⊢\varnothing \mathrm{++}\varnothing =\varnothing$$