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 syl6ibr
 |-  ( ( 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 ) )