Description: Equality deduction for intersection of two classes. (Contributed by NM, 7Feb2007)
Ref  Expression  

Hypotheses  ineq1d.1   ( ph > A = B ) 

ineqan12d.2   ( ps > C = D ) 

Assertion  ineqan12d   ( ( ph /\ ps ) > ( A i^i C ) = ( B i^i D ) ) 
Step  Hyp  Ref  Expression 

1  ineq1d.1   ( ph > A = B ) 

2  ineqan12d.2   ( ps > C = D ) 

3  ineq12   ( ( A = B /\ C = D ) > ( A i^i C ) = ( B i^i D ) ) 

4  1 2 3  syl2an   ( ( ph /\ ps ) > ( A i^i C ) = ( B i^i D ) ) 