Metamath Proof Explorer


Theorem 2alimdv

Description: Deduction form of Theorem 19.20 of Margaris p. 90 with two quantifiers, see alim . (Contributed by NM, 27-Apr-2004)

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

Proof

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