Theorem 19.30

Theorem 19.30 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Conclusion
\( \vdash \forall x \, (\varphi \vee \psi) \rightarrow \forall x \, \varphi \vee \exists x \, \psi \)
Proof
l0
exnal
\( \vdash \exists x \, \neg \varphi \leftrightarrow \neg \forall x \, \varphi \)
pm2.53
aleximi _
\( \vdash \forall x \, (\varphi \vee \psi) \rightarrow \exists x \, \neg \varphi \rightarrow \exists x \, \psi \)
biimtrrid l0 _
orrd _