Theorem mooran1

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

Conclusion
\( \vdash \exists^\ast x \, \varphi \vee \exists^\ast x \, \psi \rightarrow \exists^\ast x \, (\varphi \wedge \psi) \)
Proof
simpl
l1
moimi _
moan
jaoi l1 _