Metamath Proof Explorer


Theorem ccatlcan

Description: Concatenation of words is left-cancellative. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Assertion ccatlcan A Word X B Word X C Word X C ++ A = C ++ B A = B

Proof

Step Hyp Ref Expression
1 eqid C = C
2 ccatopth C Word X A Word X C Word X B Word X C = C C ++ A = C ++ B C = C A = B
3 1 2 mp3an3 C Word X A Word X C Word X B Word X C ++ A = C ++ B C = C A = B
4 3 3impdi C Word X A Word X B Word X C ++ A = C ++ B C = C A = B
5 4 3coml A Word X B Word X C Word X C ++ A = C ++ B C = C A = B
6 eqid C = C
7 6 biantrur A = B C = C A = B
8 5 7 bitr4di A Word X B Word X C Word X C ++ A = C ++ B A = B