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