Description: Equality deduction for class intersection. (Contributed by NM, 2Sep2003)
Ref  Expression  

Hypothesis  inteqd.1   ( ph > A = B ) 

Assertion  inteqd   ( ph > ^ A = ^ B ) 
Step  Hyp  Ref  Expression 

1  inteqd.1   ( ph > A = B ) 

2  inteq   ( A = B > ^ A = ^ B ) 

3  1 2  syl   ( ph > ^ A = ^ B ) 