Theorem 19.36iv

Inference associated with 19.36v. Version of 19.36i with a disjoint variable condition. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 17-Jan-2020.) Remove dependency on [ax-6]. (Revised by Rohan Ridenour, 15-Apr-2022.)

Hypothesis
19.36iv.1
\( \vdash \exists x \, (\varphi \rightarrow \psi) \)
Conclusion
\( \vdash \forall x \, \varphi \rightarrow \psi \)
Proof
l0
19.36iv.1
\( \vdash \exists x \, (\varphi \rightarrow \psi) \)
19.36imv
\( \vdash \exists x \, (\varphi \rightarrow \psi) \rightarrow \forall x \, \varphi \rightarrow \psi \)
ax-mp l0 _