Metamath Proof Explorer

Theorem ccatrcan

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

Ref Expression
Assertion ccatrcan ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X → A ++ C = B ++ C ↔ A = B

Proof

Step Hyp Ref Expression
1 eqid ⊢ C = C
2 ccatopth2 ⊢ A ∈ Word X ∧ C ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X ∧ C = C → A ++ C = B ++ C ↔ A = B ∧ C = C
3 1 2 mp3an3 ⊢ A ∈ Word X ∧ C ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X → A ++ C = B ++ C ↔ A = B ∧ C = C
4 3 3impdir ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X → A ++ C = B ++ C ↔ A = B ∧ C = C
5 eqid ⊢ C = C
6 5 biantru ⊢ A = B ↔ A = B ∧ C = C
7 4 6 bitr4di ⊢ A ∈ Word X ∧ B ∈ Word X ∧ C ∈ Word X → A ++ C = B ++ C ↔ A = B