Theorem bj-almp 36832

Description: A quantified form of ax-mp 5. See also barbara 2664, bj-almpi 36834, and the inference associated with ala1 1815. (Contributed by BJ, 19-Mar-2026.) (Proof modification is discouraged.)

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 1812	. 2 ⊢ (∀𝑥(𝜓 → 𝜑) → (∀𝑥𝜓 → ∀𝑥𝜑))
4	1, 2, 3	mp2 9	1 ⊢ ∀𝑥𝜑

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-4 1811

This theorem is referenced by:  bj-alimii  36833  bj-almpi  36834  bj-axseprep  37313