Metamath Proof Explorer

Theorem ccatrcan

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

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

Proof

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