Metamath Proof Explorer

Theorem eleq12d

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994)

Ref Expression
Hypotheses eleq12d.1 φ A = B
eleq12d.2 φ C = D
Assertion eleq12d φ A C B D


Step Hyp Ref Expression
1 eleq12d.1 φ A = B
2 eleq12d.2 φ C = D
3 2 eleq2d φ A C A D
4 1 eleq1d φ A D B D
5 3 4 bitrd φ A C B D