Metamath Proof Explorer

Theorem ccatrcan

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

Ref Expression
Assertion ccatrcan 
|- ( ( A e. Word X /\ B e. Word X /\ C e. Word X ) -> ( ( A ++ C ) = ( B ++ C ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( # ` C ) = ( # ` C )
2 ccatopth2 
 |-  ( ( ( A e. Word X /\ C e. Word X ) /\ ( B e. Word X /\ C e. Word X ) /\ ( # ` C ) = ( # ` C ) ) -> ( ( A ++ C ) = ( B ++ C ) <-> ( A = B /\ C = C ) ) )
3 1 2 mp3an3 
 |-  ( ( ( A e. Word X /\ C e. Word X ) /\ ( B e. Word X /\ C e. Word X ) ) -> ( ( A ++ C ) = ( B ++ C ) <-> ( A = B /\ C = C ) ) )
4 3 3impdir 
 |-  ( ( A e. Word X /\ B e. Word X /\ C e. 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 e. Word X /\ B e. Word X /\ C e. Word X ) -> ( ( A ++ C ) = ( B ++ C ) <-> A = B ) )