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

Metamath Proof Explorer

Theorem eqeq12i

Description: A useful inference for substituting definitions into an equality. (Contributed by NM, 15-Jul-1993) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof shortened by Wolf Lammen, 20-Nov-2019)

Ref Expression
Hypotheses eqeq12i.1 ⊢ A = B
eqeq12i.2 ⊢ C = D
Assertion eqeq12i ⊢ A = C ↔ B = D

Proof

Step Hyp Ref Expression
1 eqeq12i.1 ⊢ A = B
2 eqeq12i.2 ⊢ C = D
3 1 eqeq1i ⊢ A = C ↔ B = C
4 2 eqeq2i ⊢ B = C ↔ B = D
5 3 4 bitri ⊢ A = C ↔ B = D