Description: Inference removing two universal quantifiers. Version of 19.21bi with two quantifiers. (Contributed by NM, 20Apr1994)
Ref  Expression  

Hypothesis  19.21bbi.1   ( ph > A. x A. y ps ) 

Assertion  19.21bbi   ( ph > ps ) 
Step  Hyp  Ref  Expression 

1  19.21bbi.1   ( ph > A. x A. y ps ) 

2  1  19.21bi   ( ph > A. y ps ) 
3  2  19.21bi   ( ph > ps ) 