Metamath Proof Explorer

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 
 |-  (/) e. Word _V
2 ccatlid 
 |-  ( (/) e. Word _V -> ( (/) ++ (/) ) = (/) )
3 1 2 ax-mp 
 |-  ( (/) ++ (/) ) = (/)