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	⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ) ∧ ∃x(φ ∧ χ)) → ∃x(φ ∧ ψ ∧ χ))

Proof of Theorem mopick2

Step	Hyp	Ref	Expression
1		pm3.26 256	. . . . 5 ⊢ ((φ ∧ ψ) → φ)
2	1	19.22i 723	. . . 4 ⊢ (∃x(φ ∧ ψ) → ∃xφ)
3	2	adantl 305	. . 3 ⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ)) → ∃xφ)
4	3	3adant3 599	. 2 ⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ) ∧ ∃x(φ ∧ χ)) → ∃xφ)
5		hbmo1 1032	. . . 4 ⊢ (∃*xφ → ∀x∃*xφ)
6		hbe1 709	. . . 4 ⊢ (∃x(φ ∧ ψ) → ∀x∃x(φ ∧ ψ))
7		hbe1 709	. . . 4 ⊢ (∃x(φ ∧ χ) → ∀x∃x(φ ∧ χ))
8	5, 6, 7	hb3an 707	. . 3 ⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ) ∧ ∃x(φ ∧ χ)) → ∀x(∃*xφ ∧ ∃x(φ ∧ ψ) ∧ ∃x(φ ∧ χ)))
9		mopick 1054	. . . . . . 7 ⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ)) → (φ → ψ))
10		mopick 1054	. . . . . . 7 ⊢ ((∃*xφ ∧ ∃x(φ ∧ χ)) → (φ → χ))
11	9, 10	anim12i 268	. . . . . 6 ⊢ (((∃*xφ ∧ ∃x(φ ∧ ψ)) ∧ (∃*xφ ∧ ∃x(φ ∧ χ))) → ((φ → ψ) ∧ (φ → χ)))
12		3anass 585	. . . . . . 7 ⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ) ∧ ∃x(φ ∧ χ)) ↔ (∃*xφ ∧ (∃x(φ ∧ ψ) ∧ ∃x(φ ∧ χ))))
13		anandi 392	. . . . . . 7 ⊢ ((∃*xφ ∧ (∃x(φ ∧ ψ) ∧ ∃x(φ ∧ χ))) ↔ ((∃*xφ ∧ ∃x(φ ∧ ψ)) ∧ (∃*xφ ∧ ∃x(φ ∧ χ))))
14	12, 13	bitr 151	. . . . . 6 ⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ) ∧ ∃x(φ ∧ χ)) ↔ ((∃*xφ ∧ ∃x(φ ∧ ψ)) ∧ (∃*xφ ∧ ∃x(φ ∧ χ))))
15		jcab 454	. . . . . 6 ⊢ ((φ → (ψ ∧ χ)) ↔ ((φ → ψ) ∧ (φ → χ)))
16	11, 14, 15	3imtr4 192	. . . . 5 ⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ) ∧ ∃x(φ ∧ χ)) → (φ → (ψ ∧ χ)))
17	16	ancld 246	. . . 4 ⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ) ∧ ∃x(φ ∧ χ)) → (φ → (φ ∧ (ψ ∧ χ))))
18		3anass 585	. . . 4 ⊢ ((φ ∧ ψ ∧ χ) ↔ (φ ∧ (ψ ∧ χ)))
19	17, 18	syl6ibr 186	. . 3 ⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ) ∧ ∃x(φ ∧ χ)) → (φ → (φ ∧ ψ ∧ χ)))
20	8, 19	19.22d 744	. 2 ⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ) ∧ ∃x(φ ∧ χ)) → (∃xφ → ∃x(φ ∧ ψ ∧ χ)))
21	4, 20	mpd 46	1 ⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ) ∧ ∃x(φ ∧ χ)) → ∃x(φ ∧ ψ ∧ χ))

Syntax hints:   → wi 2   ∧ wa 196   ∧ w3a 581  ∃wex 678  ∃*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