Metamath Proof Explorer

Theorem eqeq12OLD

Description: Obsolete version of eqeq12 as of 23-Oct-2024. (Contributed by NM, 3-Aug-1994) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion eqeq12OLD ⊢ A = B ∧ C = D → A = C ↔ B = D

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ A = B → A = C ↔ B = C
2 eqeq2 ⊢ C = D → B = C ↔ B = D
3 1 2 sylan9bb ⊢ A = B ∧ C = D → A = C ↔ B = D