Theorem 19.41v 1901

Description: Version of 19.41 2090 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)

Assertion

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

Distinct variable group:   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 19.41v

Step	Hyp	Ref	Expression
1		19.40 1785	. . 3 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ ∃𝑥𝜓))
2		19.9v 1883	. . . 4 ⊢ (∃𝑥𝜓 ↔ 𝜓)
3	2	anbi2i 726	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))
4	1, 3	sylib 207	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) → (∃𝑥𝜑 ∧ 𝜓))
5		pm3.21 463	. . . 4 ⊢ (𝜓 → (𝜑 → (𝜑 ∧ 𝜓)))
6	5	eximdv 1833	. . 3 ⊢ (𝜓 → (∃𝑥𝜑 → ∃𝑥(𝜑 ∧ 𝜓)))
7	6	impcom 445	. 2 ⊢ ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓))
8	4, 7	impbii 198	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696

This theorem is referenced by:  19.41vv  1902  19.41vvv  1903  19.41vvvv  1904  19.42v  1905  equsexvw  1919  r19.41v  3070  gencbvex  3223  euxfr  3359  euind  3360  zfpair  4831  opabn0  4931  eliunxp  5181  relop  5194  dmuni  5256  dmres  5339  dminss  5466  imainss  5467  ssrnres  5491  cnvresima  5541  resco  5556  rnco  5558  coass  5571  xpco  5592  rnoprab  6641  f11o  7021  frxp  7174  omeu  7552  domen  7854  xpassen  7939  kmlem3  8857  cflem  8951  genpass  9710  ltexprlem4  9740  hasheqf1oi  13002  hasheqf1oiOLD  13003  3v3e3cycl2  26192  bnj534  30062  bnj906  30254  bnj908  30255  bnj916  30257  bnj983  30275  bnj986  30278  dftr6  30893  bj-eeanvw  31891  bj-csbsnlem  32090  bj-rest10  32222  bj-restuni  32231  bj-ccinftydisj  32277  prter2  33184  dihglb2  35649  pm11.6  37614  pm11.71  37619  rfcnnnub  38218  elwspths2spth  41171  eliunxp2  41905