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 φACBD

Proof

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