Theorem mooran2

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

	Ref	Expression
Assertion	mooran2	$$⊢{\exists }^{*}x\left(\phi \vee \psi \right)\to \left({\exists }^{*}x\phi \wedge {\exists }^{*}x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		moor	$$⊢{\exists }^{*}x\left(\phi \vee \psi \right)\to {\exists }^{*}x\phi$$
2		olc	$$⊢\psi \to \left(\phi \vee \psi \right)$$
3	2	moimi	$$⊢{\exists }^{*}x\left(\phi \vee \psi \right)\to {\exists }^{*}x\psi$$
4	1 3	jca	$$⊢{\exists }^{*}x\left(\phi \vee \psi \right)\to \left({\exists }^{*}x\phi \wedge {\exists }^{*}x\psi \right)$$