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 𝐴 = 𝐵
eqeq12i.2 𝐶 = 𝐷
Assertion eqeq12i ( 𝐴 = 𝐶𝐵 = 𝐷 )

Proof

Step Hyp Ref Expression
1 eqeq12i.1 𝐴 = 𝐵
2 eqeq12i.2 𝐶 = 𝐷
3 1 eqeq1i ( 𝐴 = 𝐶𝐵 = 𝐶 )
4 2 eqeq2i ( 𝐵 = 𝐶𝐵 = 𝐷 )
5 3 4 bitri ( 𝐴 = 𝐶𝐵 = 𝐷 )