Theorem al3im 41144

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

Assertion

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

Proof of Theorem al3im

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

Syntax hints:   → wi 4  ∀wal 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 1813

This theorem is referenced by: (None)