Theorem bj-alsyl 37255

Description: Syllogism under the universal quantifier, in the curried form appearing as Theorem *10.3 of [WhiteheadRussell] p. 145. See alsyl 1926 for the uncurried form. (Contributed by BJ, 28-Mar-2026.)

Assertion

Ref	Expression
bj-alsyl	⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥(𝜓 → 𝜒) → ∀𝑥(𝜑 → 𝜒)))

Proof of Theorem bj-alsyl

Step	Hyp	Ref	Expression
1		imim1 84	. 2 ⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
2	1	al2imi 1848	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-gen 1828  ax-4 1842

This theorem is used by: (None)