Theorem mooran2

"At most one" exports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)

Conclusion
\( \vdash \exists^\ast x \, (\varphi \vee \psi) \rightarrow \exists^\ast x \, \varphi \wedge \exists^\ast x \, \psi \)
Proof
l0
moor
olc
moimi _
jca l0 _