Metamath Proof Explorer

Theorem ccatlcan

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

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

Proof

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