Metamath Proof Explorer


Theorem ralimia

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996)

Ref Expression
Hypothesis ralimia.1
|- ( x e. A -> ( ph -> ps ) )
Assertion ralimia
|- ( A. x e. A ph -> A. x e. A ps )

Proof

Step Hyp Ref Expression
1 ralimia.1
 |-  ( x e. A -> ( ph -> ps ) )
2 1 a2i
 |-  ( ( x e. A -> ph ) -> ( x e. A -> ps ) )
3 2 ralimi2
 |-  ( A. x e. A ph -> A. x e. A ps )