Theorem 19.40b

The antecedent provides a condition implying the converse of 19.40. This is to 19.40 what 19.33b is to 19.33. (Contributed by BJ, 6-May-2019.) (Proof shortened by Wolf Lammen, 13-Nov-2020.)

Conclusion
\( \vdash \forall x \, \varphi \vee \forall x \, \psi \rightarrow (\exists x \, \varphi \wedge \exists x \, \psi \leftrightarrow \exists x \, (\varphi \wedge \psi)) \)
Proof
pm3.21
l1
aleximi _
pm3.2
aleximi _
jaoa l1 _
l5
orcoms _
19.40
impbid1 l5 _