Metamath Proof Explorer

Theorem moan

Description: "At most one" is still the case when a conjunct is added. (Contributed by NM, 22-Apr-1995)

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ps /\ ph ) -> ph )
2 1 moimi 
 |-  ( E* x ph -> E* x ( ps /\ ph ) )