Description: A membership and equality inference. (Contributed by NM, 4Jan2006)
Ref  Expression  

Hypotheses  eqeltrid.1   A = B 

eqeltrid.2   ( ph > B e. C ) 

Assertion  eqeltrid   ( ph > A e. C ) 
Step  Hyp  Ref  Expression 

1  eqeltrid.1   A = B 

2  eqeltrid.2   ( ph > B e. C ) 

3  1  a1i   ( ph > A = B ) 
4  3 2  eqeltrd   ( ph > A e. C ) 