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

Metamath Proof Explorer

Theorem eqeqan12dALT

Description: Alternate proof of eqeqan12d . This proof has one more step but one fewer essential step. (Contributed by NM, 9-Aug-1994) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 eqeqan12dALT.1 ⊢ φ → A = B
2 eqeqan12dALT.2 ⊢ ψ → C = D
3 eqeq12 ⊢ A = B ∧ C = D → A = C ↔ B = D
4 1 2 3 syl2an ⊢ φ ∧ ψ → A = C ↔ B = D