Theorem 19.36

Description: Theorem 19.36 of Margaris p. 90. See 19.36v for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993)

	Ref	Expression
Hypothesis	19.36.1	$$⊢Ⅎx\psi$$
Assertion	19.36	$$⊢\exists x\left(\phi \to \psi \right)\leftrightarrow \left(\forall x\phi \to \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		19.36.1	$$⊢Ⅎx\psi$$
2		19.35	$$⊢\exists x\left(\phi \to \psi \right)\leftrightarrow \left(\forall x\phi \to \exists x\psi \right)$$
3	1	19.9	$$⊢\exists x\psi \leftrightarrow \psi$$
4	3	imbi2i	$$⊢\left(\forall x\phi \to \exists x\psi \right)\leftrightarrow \left(\forall x\phi \to \psi \right)$$
5	2 4	bitri	$$⊢\exists x\left(\phi \to \psi \right)\leftrightarrow \left(\forall x\phi \to \psi \right)$$