This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem caovcanrd

Description: Commute the arguments of an operation cancellation law. (Contributed by Mario Carneiro, 30-Dec-2014)

Ref Expression
Hypotheses caovcang.1 
|- ( ( ph /\ ( x e. T /\ y e. S /\ z e. S ) ) -> ( ( x F y ) = ( x F z ) <-> y = z ) )
caovcand.2 
|- ( ph -> A e. T )
caovcand.3 
|- ( ph -> B e. S )
caovcand.4 
|- ( ph -> C e. S )
caovcanrd.5 
|- ( ph -> A e. S )
caovcanrd.6 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )
Assertion caovcanrd 
|- ( ph -> ( ( B F A ) = ( C F A ) <-> B = C ) )

Proof

Step Hyp Ref Expression
1 caovcang.1 
 |-  ( ( ph /\ ( x e. T /\ y e. S /\ z e. S ) ) -> ( ( x F y ) = ( x F z ) <-> y = z ) )
2 caovcand.2 
 |-  ( ph -> A e. T )
3 caovcand.3 
 |-  ( ph -> B e. S )
4 caovcand.4 
 |-  ( ph -> C e. S )
5 caovcanrd.5 
 |-  ( ph -> A e. S )
6 caovcanrd.6 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x F y ) = ( y F x ) )
7 6 5 3 caovcomd 
 |-  ( ph -> ( A F B ) = ( B F A ) )
8 6 5 4 caovcomd 
 |-  ( ph -> ( A F C ) = ( C F A ) )
9 7 8 eqeq12d 
 |-  ( ph -> ( ( A F B ) = ( A F C ) <-> ( B F A ) = ( C F A ) ) )
10 1 2 3 4 caovcand 
 |-  ( ph -> ( ( A F B ) = ( A F C ) <-> B = C ) )
11 9 10 bitr3d 
 |-  ( ph -> ( ( B F A ) = ( C F A ) <-> B = C ) )