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

Metamath Proof Explorer

Theorem eqeqan2d

Description: Implication of introducing a new equality. (Contributed by Peter Mazsa, 17-Apr-2019)

Ref Expression
Hypothesis eqeqan2d.1 ⊢ φ → C = D
Assertion eqeqan2d ⊢ A = B ∧ φ → A = C ↔ B = D

Proof

Step Hyp Ref Expression
1 eqeqan2d.1 ⊢ φ → C = D
2 eqeq12 ⊢ A = B ∧ C = D → A = C ↔ B = D
3 1 2 sylan2 ⊢ A = B ∧ φ → A = C ↔ B = D