Theorem mopick2 1057

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 773.

Assertion

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

Proof of Theorem mopick2

Step	Hyp	Ref	Expression
1		pm3.26 256	. . . . 5 |- ((ph /\ ps) -> ph)
2	1	19.22i 723	. . . 4 |- (E.x(ph /\ ps) -> E.xph)
3	2	adantl 305	. . 3 |- ((E*xph /\ E.x(ph /\ ps)) -> E.xph)
4	3	3adant3 599	. 2 |- ((E*xph /\ E.x(ph /\ ps) /\ E.x(ph /\ ch)) -> E.xph)
5		hbmo1 1032	. . . 4 |- (E*xph -> A.xE*xph)
6		hbe1 709	. . . 4 |- (E.x(ph /\ ps) -> A.xE.x(ph /\ ps))
7		hbe1 709	. . . 4 |- (E.x(ph /\ ch) -> A.xE.x(ph /\ ch))
8	5, 6, 7	hb3an 707	. . 3 |- ((E*xph /\ E.x(ph /\ ps) /\ E.x(ph /\ ch)) -> A.x(E*xph /\ E.x(ph /\ ps) /\ E.x(ph /\ ch)))
9		mopick 1054	. . . . . . 7 |- ((E*xph /\ E.x(ph /\ ps)) -> (ph -> ps))
10		mopick 1054	. . . . . . 7 |- ((E*xph /\ E.x(ph /\ ch)) -> (ph -> ch))
11	9, 10	anim12i 268	. . . . . 6 |- (((E*xph /\ E.x(ph /\ ps)) /\ (E*xph /\ E.x(ph /\ ch))) -> ((ph -> ps) /\ (ph -> ch)))
12		3anass 585	. . . . . . 7 |- ((E*xph /\ E.x(ph /\ ps) /\ E.x(ph /\ ch)) <-> (E*xph /\ (E.x(ph /\ ps) /\ E.x(ph /\ ch))))
13		anandi 392	. . . . . . 7 |- ((E*xph /\ (E.x(ph /\ ps) /\ E.x(ph /\ ch))) <-> ((E*xph /\ E.x(ph /\ ps)) /\ (E*xph /\ E.x(ph /\ ch))))
14	12, 13	bitr 151	. . . . . 6 |- ((E*xph /\ E.x(ph /\ ps) /\ E.x(ph /\ ch)) <-> ((E*xph /\ E.x(ph /\ ps)) /\ (E*xph /\ E.x(ph /\ ch))))
15		jcab 454	. . . . . 6 |- ((ph -> (ps /\ ch)) <-> ((ph -> ps) /\ (ph -> ch)))
16	11, 14, 15	3imtr4 192	. . . . 5 |- ((E*xph /\ E.x(ph /\ ps) /\ E.x(ph /\ ch)) -> (ph -> (ps /\ ch)))
17	16	ancld 246	. . . 4 |- ((E*xph /\ E.x(ph /\ ps) /\ E.x(ph /\ ch)) -> (ph -> (ph /\ (ps /\ ch))))
18		3anass 585	. . . 4 |- ((ph /\ ps /\ ch) <-> (ph /\ (ps /\ ch)))
19	17, 18	syl6ibr 186	. . 3 |- ((E*xph /\ E.x(ph /\ ps) /\ E.x(ph /\ ch)) -> (ph -> (ph /\ ps /\ ch)))
20	8, 19	19.22d 744	. 2 |- ((E*xph /\ E.x(ph /\ ps) /\ E.x(ph /\ ch)) -> (E.xph -> E.x(ph /\ ps /\ ch)))
21	4, 20	mpd 46	1 |- ((E*xph /\ E.x(ph /\ ps) /\ E.x(ph /\ ch)) -> E.x(ph /\ ps /\ ch))

Syntax hints:   -> wi 2   /\ wa 196   /\ w3a 581  E.wex 678  E*wmo 1008

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010

metamath.org