Theorem al3im

Description: Version of ax-4 for a nested implication. (Contributed by RP, 13-Apr-2020)

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

Proof

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