Metamath Proof Explorer


Theorem eleqtrdi

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006)

Ref Expression
Hypotheses eleqtrdi.1 φAB
eleqtrdi.2 B=C
Assertion eleqtrdi φAC

Proof

Step Hyp Ref Expression
1 eleqtrdi.1 φAB
2 eleqtrdi.2 B=C
3 2 a1i φB=C
4 1 3 eleqtrd φAC