Theorem 19.42v 2033

Description: Version of 19.42 2261 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 2029	. 2 ⊢ (∃𝑥(𝜓 ∧ 𝜑) ↔ (∃𝑥𝜓 ∧ 𝜑))
2		exancom 1938	. 2 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜓 ∧ 𝜑))
3		ancom 452	. 2 ⊢ ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓 ∧ 𝜑))
4	1, 2, 3	3bitr4i 292	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))

Syntax hints:   ↔ wb 196   ∧ wa 382  ∃wex 1852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853

This theorem is referenced by:  exdistr  2034  19.42vv  2035  19.42vvv  2036  4exdistr  2039  2sb5  2276  eeeanv  2345  rexcom4a  3378  ceqsex2  3396  reuind  3563  2reu5lem3  3567  sbccomlem  3658  bm1.3ii  4918  eqvinop  5082  dmopabss  5474  dmopab3  5475  mptpreima  5772  mptfnf  6155  brprcneu  6325  fndmin  6467  fliftf  6708  dfoprab2  6848  dmoprab  6888  dmoprabss  6889  fnoprabg  6908  uniuni  7118  zfrep6  7281  opabex3d  7292  opabex3  7293  fsplit  7433  eroveu  7995  rankuni  8890  aceq1  9140  dfac3  9144  kmlem14  9187  kmlem15  9188  axdc2lem  9472  1idpr  10053  ltexprlem1  10060  ltexprlem4  10063  xpcogend  13923  shftdm  14019  joindm  17211  meetdm  17225  toprntopon  20950  ntreq0  21102  cnextf  22090  adjeu  29088  rexunirn  29670  fpwrelmapffslem  29847  tgoldbachgt  31081  bnj1019  31188  bnj1209  31205  bnj1033  31375  bnj1189  31415  dmscut  32255  dfiota3  32367  brimg  32381  funpartlem  32386  bj-eeanvw  33041  bj-rexcom4  33198  bj-rexcom4a  33199  bj-snsetex  33282  bj-snglc  33288  bj-bm1.3ii  33355  bj-restuni  33382  itg2addnc  33796  sbccom2lem  34261  eldmres  34379  rnxrn  34498  rp-isfinite6  38390  undmrnresiss  38436  elintima  38471  pm11.58  39116  pm11.71  39123  2sbc5g  39143  iotasbc2  39147  ax6e2nd  39299  ax6e2ndVD  39666  ax6e2ndALT  39688  stoweidlem60  40794  elpglem3  42987