Theorem bj-spimnfe 36886

Description: A universal specification result: if 𝜑 is true for all values of 𝑥 and implies 𝜓 for at least one value, and if furthermore 𝑥 is ∃-weakly nonfree in 𝜓, then 𝜓 follows. An intermediate result on the way to prove 19.36i 2239, bj-19.36im 37028, 19.36imv 1947, spimfw 1967... (Contributed by BJ, 3-Apr-2026.) Proof should not use 19.35 1879. (Proof modification is discouraged.)

Assertion

Ref	Expression
bj-spimnfe	⊢ ((∃𝑥𝜓 → 𝜓) → (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)))

Proof of Theorem bj-spimnfe

Step	Hyp	Ref	Expression
1		bj-eximcom 36879	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
2		imim2 58	. 2 ⊢ ((∃𝑥𝜓 → 𝜓) → ((∀𝑥𝜑 → ∃𝑥𝜓) → (∀𝑥𝜑 → 𝜓)))
3	1, 2	syl5 34	1 ⊢ ((∃𝑥𝜓 → 𝜓) → (∃𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → 𝜓)))

Syntax hints:   → wi 4  ∀wal 1540  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  bj-spim  36888  bj-19.36im  37028