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 
|- <" A B C "> = ( <" A B "> ++ <" C "> )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 cB 
 |-  B
2 cC 
 |-  C
3 0 1 2 cs3 
 |-  <" A B C ">
4 0 1 cs2 
 |-  <" A B ">
5 cconcat 
 |-  ++
6 2 cs1 
 |-  <" C ">
7 4 6 5 co 
 |-  ( <" A B "> ++ <" C "> )
8 3 7 wceq 
 |-  <" A B C "> = ( <" A B "> ++ <" C "> )