Theorem al3im 44414

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

Assertion

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

Proof of Theorem al3im

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 1842

This theorem is used by: (None)