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	$$⊢Ⅎx\phi$$
	19.21-2.2	$$⊢Ⅎy\phi$$
Assertion	19.21-2	$$⊢\forall x\forall y\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \forall x\forall y\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		19.21-2.1	$$⊢Ⅎx\phi$$
2		19.21-2.2	$$⊢Ⅎy\phi$$
3	2	19.21	$$⊢\forall y\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \forall y\psi \right)$$
4	3	albii	$$⊢\forall x\forall y\left(\phi \to \psi \right)\leftrightarrow \forall x\left(\phi \to \forall y\psi \right)$$
5	1	19.21	$$⊢\forall x\left(\phi \to \forall y\psi \right)\leftrightarrow \left(\phi \to \forall x\forall y\psi \right)$$
6	4 5	bitri	$$⊢\forall x\forall y\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \forall x\forall y\psi \right)$$