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	⊢ 𝐴 = 𝐵
	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	⊢ ( 𝐴 = 𝐶 ↔ 𝐵 = 𝐷 )