Metamath Proof Explorer

Theorem eqtrb

Description: A transposition of equality. (Contributed by Thierry Arnoux, 20-Aug-2023)

Ref Expression
Assertion eqtrb 
|- ( ( A = B /\ A = C ) <-> ( A = B /\ B = C ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A = B /\ A = C ) -> A = B )
2 eqtr2 
 |-  ( ( A = B /\ A = C ) -> B = C )
3 1 2 jca 
 |-  ( ( A = B /\ A = C ) -> ( A = B /\ B = C ) )
4 simpl 
 |-  ( ( A = B /\ B = C ) -> A = B )
5 eqtr 
 |-  ( ( A = B /\ B = C ) -> A = C )
6 4 5 jca 
 |-  ( ( A = B /\ B = C ) -> ( A = B /\ A = C ) )
7 3 6 impbii 
 |-  ( ( A = B /\ A = C ) <-> ( A = B /\ B = C ) )