Metamath Proof Explorer


Theorem eqeltrrid

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

Ref Expression
Hypotheses eqeltrrid.1 B=A
eqeltrrid.2 φBC
Assertion eqeltrrid φAC

Proof

Step Hyp Ref Expression
1 eqeltrrid.1 B=A
2 eqeltrrid.2 φBC
3 1 eqcomi A=B
4 3 2 eqeltrid φAC