Theorem hbald

Description: Deduction form of bound-variable hypothesis builder hbal . (Contributed by NM, 2-Jan-2002)

	Ref	Expression
Hypotheses	hbald.1	$$⊢\phi \to \forall y\phi$$
	hbald.2	$$⊢\phi \to \left(\psi \to \forall x\psi \right)$$
Assertion	hbald	$$⊢\phi \to \left(\forall y\psi \to \forall x\forall y\psi \right)$$

Proof

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