Theorem bj-almp 37403

Description: A quantified form of ax-mp 5. See also barbara 2687, bj-ala1i 37410, bj-almpi 37411. (Contributed by BJ, 19-Mar-2026.)

Hypotheses

Ref	Expression
bj-almp.maj	⊢ ∀𝑥(𝜓 → 𝜑)
bj-almp.min	⊢ ∀𝑥𝜓

Assertion

Ref	Expression
bj-almp	⊢ ∀𝑥𝜑

Proof of Theorem bj-almp

Step	Hyp	Ref	Expression
1		bj-almp.maj	. 2 ⊢ ∀𝑥(𝜓 → 𝜑)
2		bj-almp.min	. 2 ⊢ ∀𝑥𝜓
3		alim 1843	. 2 ⊢ (∀𝑥(𝜓 → 𝜑) → (∀𝑥𝜓 → ∀𝑥𝜑))
4	1, 2, 3	mp2 9	1 ⊢ ∀𝑥𝜑

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

This proof depends on axioms:  ax-mp 5  ax-4 1842

This theorem is used by:  bj-alimii  37409  bj-almpi  37411  bj-axseprep  37910