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