Theorem bj-alimii 36833

Description: Inference associated with alimi 1813. Double inference associated with alim 1812. The usual proof of an associated inference (here from alimi 1813 and ax-mp 5) has the same size and same number of steps. (Contributed by BJ, 19-Mar-2026.) (Proof modification is discouraged.)

Hypotheses

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

Assertion

Ref	Expression
bj-alimii	⊢ ∀𝑥𝜑

Proof of Theorem bj-alimii

Step	Hyp	Ref	Expression
1		bj-alimii.maj	. . 3 ⊢ (𝜓 → 𝜑)
2	1	ax-gen 1797	. 2 ⊢ ∀𝑥(𝜓 → 𝜑)
3		bj-alimii.min	. 2 ⊢ ∀𝑥𝜓
4	2, 3	bj-almp 36832	1 ⊢ ∀𝑥𝜑

Syntax hints:   → wi 4  ∀wal 1540

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

This theorem is referenced by:  bj-axnul  37311  bj-axreprepsep  37314