Theorem 19.34

Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)

Conclusion
\( \vdash \forall x \, \varphi \vee \exists x \, \psi \rightarrow \exists x \, (\varphi \vee \psi) \)
Proof
19.2
l1
orim1i _
\( \vdash \forall x \, \varphi \vee \exists x \, \psi \rightarrow \exists x \, \varphi \vee \exists x \, \psi \)
19.43
\( \vdash \exists x \, (\varphi \vee \psi) \leftrightarrow \exists x \, \varphi \vee \exists x \, \psi \)
sylibr l1 _