Theorem hbaltg

Description: A more general and closed form of hbal . (Contributed by Scott Fenton, 13-Dec-2010)

	Ref	Expression
Assertion	hbaltg	$$⊢\forall x\left(\phi \to \forall y\psi \right)\to \left(\forall x\phi \to \forall y\forall x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		alim	$$⊢\forall x\left(\phi \to \forall y\psi \right)\to \left(\forall x\phi \to \forall x\forall y\psi \right)$$
2		ax-11	$$⊢\forall x\forall y\psi \to \forall y\forall x\psi$$
3	1 2	syl6	$$⊢\forall x\left(\phi \to \forall y\psi \right)\to \left(\forall x\phi \to \forall y\forall x\psi \right)$$