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

Metamath Proof Explorer

Theorem eqeqan12d

Description: A useful inference for substituting definitions into an equality. See also eqeqan12dALT . (Contributed by NM, 9-Aug-1994) (Proof shortened by Andrew Salmon, 25-May-2011) Shorten other proofs. (Revised by Wolf Lammen, 23-Oct-2024)

Ref Expression
Hypotheses eqeqan12d.1 ⊢ φ → A = B
eqeqan12d.2 ⊢ ψ → C = D
Assertion eqeqan12d ⊢ φ ∧ ψ → A = C ↔ B = D

Proof

Step Hyp Ref Expression
1 eqeqan12d.1 ⊢ φ → A = B
2 eqeqan12d.2 ⊢ ψ → C = D
3 1 eqeq1d ⊢ φ → A = C ↔ B = C
4 2 eqeq2d ⊢ ψ → B = C ↔ B = D
5 3 4 sylan9bb ⊢ φ ∧ ψ → A = C ↔ B = D