This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ∃* x φ ∨ ψ → ∃* x φ ∧ ∃* x ψ

Proof

Step Hyp Ref Expression
1 moor ⊢ ∃* x φ ∨ ψ → ∃* x φ
2 olc ⊢ ψ → φ ∨ ψ
3 2 moimi ⊢ ∃* x φ ∨ ψ → ∃* x ψ
4 1 3 jca ⊢ ∃* x φ ∨ ψ → ∃* x φ ∧ ∃* x ψ