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