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