Theorem bj-nnfead

Description: Nonfreeness implies the equivalent of ax5ea , deduction form. (Contributed by BJ, 2-Dec-2023)

	Ref	Expression
Hypothesis	bj-nnfead.1	$$⊢\phi \to Ⅎ\text{'}x\psi$$
Assertion	bj-nnfead	$$⊢\phi \to \left(\exists x\psi \to \forall x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-nnfead.1	$$⊢\phi \to Ⅎ\text{'}x\psi$$
2		bj-nnfea	$$⊢Ⅎ\text{'}x\psi \to \left(\exists x\psi \to \forall x\psi \right)$$
3	1 2	syl	$$⊢\phi \to \left(\exists x\psi \to \forall x\psi \right)$$