Metamath Proof Explorer

Theorem alrimivv

Description: Inference form of Theorem 19.21 of Margaris p. 90. See 19.21 and 19.21v . (Contributed by NM, 31-Jul-1995)

Ref Expression
Hypothesis alrimivv.1 
|- ( ph -> ps )
Assertion alrimivv 
|- ( ph -> A. x A. y ps )

Proof

Step Hyp Ref Expression
1 alrimivv.1 
 |-  ( ph -> ps )
2 1 alrimiv 
 |-  ( ph -> A. y ps )
3 2 alrimiv 
 |-  ( ph -> A. x A. y ps )