Metamath Proof Explorer

Theorem ccatlcan

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

Ref Expression
Assertion ccatlcan ⊢A∈WordX∧B∈WordX∧C∈WordX→C++A=C++B↔A=B

Proof

Step Hyp Ref Expression
1 eqid ⊢C=C
2 ccatopth ⊢C∈WordX∧A∈WordX∧C∈WordX∧B∈WordX∧C=C→C++A=C++B↔C=C∧A=B
3 1 2 mp3an3 ⊢C∈WordX∧A∈WordX∧C∈WordX∧B∈WordX→C++A=C++B↔C=C∧A=B
4 3 3impdi ⊢C∈WordX∧A∈WordX∧B∈WordX→C++A=C++B↔C=C∧A=B
5 4 3coml ⊢A∈WordX∧B∈WordX∧C∈WordX→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∈WordX∧B∈WordX∧C∈WordX→C++A=C++B↔A=B