Theorem 19.23v

Description: Version of 19.23 with a disjoint variable condition instead of a nonfreeness hypothesis. (Contributed by NM, 28-Jun-1998) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020) Remove dependency on ax-6 . (Revised by Rohan Ridenour, 15-Apr-2022)

	Ref	Expression
Assertion	19.23v	$$⊢\forall x\left(\phi \to \psi \right)\leftrightarrow \left(\exists x\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		exim	$$⊢\forall x\left(\phi \to \psi \right)\to \left(\exists x\phi \to \exists x\psi \right)$$
2		ax5e	$$⊢\exists x\psi \to \psi$$
3	1 2	syl6	$$⊢\forall x\left(\phi \to \psi \right)\to \left(\exists x\phi \to \psi \right)$$
4		ax-5	$$⊢\psi \to \forall x\psi$$
5	4	imim2i	$$⊢\left(\exists x\phi \to \psi \right)\to \left(\exists x\phi \to \forall x\psi \right)$$
6		19.38	$$⊢\left(\exists x\phi \to \forall x\psi \right)\to \forall x\left(\phi \to \psi \right)$$
7	5 6	syl	$$⊢\left(\exists x\phi \to \psi \right)\to \forall x\left(\phi \to \psi \right)$$
8	3 7	impbii	$$⊢\forall x\left(\phi \to \psi \right)\leftrightarrow \left(\exists x\phi \to \psi \right)$$