Metamath Proof Explorer

Theorem 2alimi

Description: Inference doubly quantifying both antecedent and consequent. (Contributed by NM, 3-Feb-2005)

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

Proof

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