Theorem al2im

Description: Closed form of al2imi . Version of alim for a nested implication. (Contributed by Alan Sare, 31-Dec-2011)

	Ref	Expression
Assertion	al2im	$$⊢\forall x\left(\phi \to \left(\psi \to \chi \right)\right)\to \left(\forall x\phi \to \left(\forall x\psi \to \forall x\chi \right)\right)$$

Proof

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