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

Metamath Proof Explorer

Theorem 19.21-2

Description: Version of 19.21 with two quantifiers. (Contributed by NM, 4-Feb-2005)

Ref Expression
Hypotheses 19.21-2.1 
|- F/ x ph
19.21-2.2 
|- F/ y ph
Assertion 19.21-2 
|- ( A. x A. y ( ph -> ps ) <-> ( ph -> A. x A. y ps ) )

Proof

Step Hyp Ref Expression
1 19.21-2.1 
 |-  F/ x ph
2 19.21-2.2 
 |-  F/ y ph
3 2 19.21 
 |-  ( A. y ( ph -> ps ) <-> ( ph -> A. y ps ) )
4 3 albii 
 |-  ( A. x A. y ( ph -> ps ) <-> A. x ( ph -> A. y ps ) )
5 1 19.21 
 |-  ( A. x ( ph -> A. y ps ) <-> ( ph -> A. x A. y ps ) )
6 4 5 bitri 
 |-  ( A. x A. y ( ph -> ps ) <-> ( ph -> A. x A. y ps ) )