Theorem bj-alimii 37238

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

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 1824	. 2 ⊢ ∀𝑥(𝜓 → 𝜑)
3		bj-alimii.min	. 2 ⊢ ∀𝑥𝜓
4	2, 3	bj-almp 37232	1 ⊢ ∀𝑥𝜑

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

This proof depends on axioms:  ax-mp 5  ax-gen 1824  ax-4 1838

This theorem is used by:  bj-axnul  37737  bj-axreprepsep  37740