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

Metamath Proof Explorer

Definition df-s4

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

Ref Expression
Assertion df-s4 ⊢ ⟨“ ABCD ”⟩ = ⟨“ ABC ”⟩ ++ ⟨“ D ”⟩

Detailed syntax breakdown

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