Metamath Proof Explorer

Theorem mopick2

Description: "At most one" can show the existence of a common value. In this case we can infer existence of conjunction from a conjunction of existence, and it is one way to achieve the converse of 19.40 . (Contributed by NM, 5-Apr-2004) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Assertion mopick2 
|- ( ( E* x ph /\ E. x ( ph /\ ps ) /\ E. x ( ph /\ ch ) ) -> E. x ( ph /\ ps /\ ch ) )

Proof

Step Hyp Ref Expression
1 nfmo1 
 |-  F/ x E* x ph
2 nfe1 
 |-  F/ x E. x ( ph /\ ps )
3 1 2 nfan 
 |-  F/ x ( E* x ph /\ E. x ( ph /\ ps ) )
4 mopick 
 |-  ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) )
5 4 ancld 
 |-  ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ( ph /\ ps ) ) )
6 5 anim1d 
 |-  ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ( ph /\ ch ) -> ( ( ph /\ ps ) /\ ch ) ) )
7 df-3an 
 |-  ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
8 6 7 imbitrrdi 
 |-  ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ( ph /\ ch ) -> ( ph /\ ps /\ ch ) ) )
9 3 8 eximd 
 |-  ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( E. x ( ph /\ ch ) -> E. x ( ph /\ ps /\ ch ) ) )
10 9 3impia 
 |-  ( ( E* x ph /\ E. x ( ph /\ ps ) /\ E. x ( ph /\ ch ) ) -> E. x ( ph /\ ps /\ ch ) )