Theorem al3im

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

	Ref	Expression
Assertion	al3im	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) ) → ( ∀ 𝑥 𝜑 → ( ∀ 𝑥 𝜓 → ( ∀ 𝑥 𝜒 → ∀ 𝑥 𝜃 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		alim	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) ) → ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( 𝜓 → ( 𝜒 → 𝜃 ) ) ) )
2		al2im	⊢ ( ∀ 𝑥 ( 𝜓 → ( 𝜒 → 𝜃 ) ) → ( ∀ 𝑥 𝜓 → ( ∀ 𝑥 𝜒 → ∀ 𝑥 𝜃 ) ) )
3	1 2	syl6	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) ) → ( ∀ 𝑥 𝜑 → ( ∀ 𝑥 𝜓 → ( ∀ 𝑥 𝜒 → ∀ 𝑥 𝜃 ) ) ) )