Theorem 19.42v 1905

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

Assertion

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

Distinct variable group:   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem 19.42v

Step	Hyp	Ref	Expression
1		19.41v 1901	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑))
2		exancom 1774	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 465	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 291	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:  exdistr  1906  19.42vv  1907  19.42vvv  1908  4exdistr  1911  eeeanv  2171  2sb5  2431  rexcom4a  3199  ceqsex2  3217  reuind  3378  2reu5lem3  3382  sbccomlem  3475  bm1.3ii  4712  eqvinop  4881  dmopabss  5258  dmopab3  5259  mptpreima  5545  mptfnf  5928  brprcneu  6096  fndmin  6232  fliftf  6465  dfoprab2  6599  dmoprab  6639  dmoprabss  6640  fnoprabg  6659  uniuni  6865  zfrep6  7027  opabex3d  7037  opabex3  7038  fsplit  7169  eroveu  7729  rankuni  8609  aceq1  8823  dfac3  8827  kmlem14  8868  kmlem15  8869  axdc2lem  9153  1idpr  9730  ltexprlem1  9737  ltexprlem4  9740  xpcogend  13561  shftdm  13659  joindm  16826  meetdm  16840  ntreq0  20691  cnextf  21680  usg2spot2nb  26592  adjeu  28132  rexunirn  28715  fpwrelmapffslem  28895  bnj1019  30104  bnj1209  30121  bnj1033  30291  bnj1189  30331  dfiota3  31200  brimg  31214  funpartlem  31219  bj-eeanvw  31891  bj-rexcom4  32063  bj-rexcom4a  32064  bj-snsetex  32144  bj-snglc  32150  bj-restuni  32231  bj-toprntopon  32244  itg2addnc  32634  sbccom2lem  33099  rp-isfinite6  36883  undmrnresiss  36929  elintima  36964  pm11.58  37612  pm11.71  37619  2sbc5g  37639  iotasbc2  37643  ax6e2nd  37795  ax6e2ndVD  38166  ax6e2ndALT  38188  stoweidlem60  38953  fusgr2wsp2nb  41498  elpglem3  42255