Metamath Proof Explorer
Description: Inference form of Theorem 19.21 of Margaris p. 90. See 19.21 and
19.21v . (Contributed by NM, 21Jun1993)


Ref 
Expression 

Hypothesis 
alrimiv.1 
 ( ph > ps ) 

Assertion 
alrimiv 
 ( ph > A. x ps ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

alrimiv.1 
 ( ph > ps ) 
2 

ax5 
 ( ph > A. x ph ) 
3 
2 1

alrimih 
 ( ph > A. x ps ) 