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 
|- ( E* x ( ph \/ ps ) -> ( E* x ph /\ E* x ps ) )

Proof

Step Hyp Ref Expression
1 moor 
 |-  ( E* x ( ph \/ ps ) -> E* x ph )
2 olc 
 |-  ( ps -> ( ph \/ ps ) )
3 2 moimi 
 |-  ( E* x ( ph \/ ps ) -> E* x ps )
4 1 3 jca 
 |-  ( E* x ( ph \/ ps ) -> ( E* x ph /\ E* x ps ) )