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  5794  dfopab2  8006  dfoprab3s  8007  xpcomco  9007  mpomptxf  32768  bnj605  35083  bnj607  35092  2sb5nd  44916  2sb5ndVD  45265  2sb5ndALT  45287  eliunxp2  48694