Theorem bj-alimii 37529

Description: Inference associated with alimi 1843. Double inference associated with alim 1842. The usual proof of an associated inference (here from alimi 1843 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 1827	. 2 ⊢ ∀𝑥(𝜓 → 𝜑)
3		bj-alimii.min	. 2 ⊢ ∀𝑥𝜓
4	2, 3	bj-almp 37523	1 ⊢ ∀𝑥𝜑

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

This proof depends on axioms:  ax-mp 5  ax-gen 1827  ax-4 1841

This theorem is used by:  bj-axnul  38030  bj-axreprepsep  38033