Metamath Proof Explorer

Theorem mooran1

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

Ref Expression
Assertion mooran1 
|- ( ( E* x ph \/ E* x ps ) -> E* x ( ph /\ ps ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( ph /\ ps ) -> ph )
2 1 moimi 
 |-  ( E* x ph -> E* x ( ph /\ ps ) )
3 moan 
 |-  ( E* x ps -> E* x ( ph /\ ps ) )
4 2 3 jaoi 
 |-  ( ( E* x ph \/ E* x ps ) -> E* x ( ph /\ ps ) )