This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ∅ ∈ Word V
2 ccatlid ⊢ ∅ ∈ Word V → ∅ ++ ∅ = ∅
3 1 2 ax-mp ⊢ ∅ ++ ∅ = ∅