Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4Mar1997)
Ref  Expression  

Hypothesis  ralimi.1   ( ph > ps ) 

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

1  ralimi.1   ( ph > ps ) 

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