Theorem 19.41 2243

Description: Theorem 19.41 of [Margaris] p. 90. See 19.41v 1951 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-Jan-2018.)

Hypothesis

Ref	Expression
19.41.1	⊢ Ⅎ𝑥𝜓

Assertion

Ref	Expression
19.41	⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Proof of Theorem 19.41

Step	Hyp	Ref	Expression
1		19.40 1888	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		19.41.1	. . . . 5 ⊢ Ⅎ𝑥𝜓
3	2	19.9 2213	. . . 4 ⊢ (∃𝑥𝜓 ↔ 𝜓)
4	3	anbi2i 624	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))
5	1, 4	sylib 218	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
6		pm3.21 471	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
7	2, 6	eximd 2224	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
8	7	impcom 407	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
9	5, 8	impbii 209	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1781  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786

This theorem is referenced by:  19.42  2244  eean  2353  eeeanv  2355  equsexALT  2424  2sb5rf  2477  r19.41  3242  eliunxp  5784  dfopab2  7996  dfoprab3s  7997  xpcomco  8996  mpomptxf  32740  bnj605  35055  bnj607  35064  2sb5nd  44990  2sb5ndVD  45339  2sb5ndALT  45361  eliunxp2  48768