Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 18Oct1996)
Ref  Expression  

Hypothesis  reximi.1   ( ph > ps ) 

Assertion  reximi   ( E. x e. A ph > E. x e. A ps ) 
Step  Hyp  Ref  Expression 

1  reximi.1   ( ph > ps ) 

2  1  a1i   ( x e. A > ( ph > ps ) ) 
3  2  reximia   ( E. x e. A ph > E. x e. A ps ) 