This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )