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

Metamath Proof Explorer

Definition df-s3

Description: Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion df-s3 ⊢ ⟨“ ABC ”⟩ = ⟨“ AB ”⟩ ++ ⟨“ C ”⟩

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 cB class B
2 cC class C
3 0 1 2 cs3 class ⟨“ ABC ”⟩
4 0 1 cs2 class ⟨“ AB ”⟩
5 cconcat class ++
6 2 cs1 class ⟨“ C ”⟩
7 4 6 5 co class ⟨“ AB ”⟩ ++ ⟨“ C ”⟩
8 3 7 wceq wff ⟨“ ABC ”⟩ = ⟨“ AB ”⟩ ++ ⟨“ C ”⟩