Theorem 19.42v 1921

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

Syntax hints:   ↔ wb 196   ∧ wa 383  ∃wex 1744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745

This theorem is referenced by:  exdistr  1922  19.42vv  1923  19.42vvv  1924  4exdistr  1927  eeeanv  2219  2sb5  2471  rexcom4a  3257  ceqsex2  3275  reuind  3444  2reu5lem3  3448  sbccomlem  3541  bm1.3ii  4817  eqvinop  4984  dmopabss  5368  dmopab3  5369  mptpreima  5666  mptfnf  6053  brprcneu  6222  fndmin  6364  fliftf  6605  dfoprab2  6743  dmoprab  6783  dmoprabss  6784  fnoprabg  6803  uniuni  7013  zfrep6  7176  opabex3d  7187  opabex3  7188  fsplit  7327  eroveu  7885  rankuni  8764  aceq1  8978  dfac3  8982  kmlem14  9023  kmlem15  9024  axdc2lem  9308  1idpr  9889  ltexprlem1  9896  ltexprlem4  9899  xpcogend  13759  shftdm  13855  joindm  17050  meetdm  17064  toprntopon  20777  ntreq0  20929  cnextf  21917  adjeu  28876  rexunirn  29458  fpwrelmapffslem  29635  tgoldbachgt  30869  bnj1019  30976  bnj1209  30993  bnj1033  31163  bnj1189  31203  dmscut  32043  dfiota3  32155  brimg  32169  funpartlem  32174  bj-eeanvw  32829  bj-rexcom4  32994  bj-rexcom4a  32995  bj-snsetex  33076  bj-snglc  33082  bj-restuni  33175  itg2addnc  33594  sbccom2lem  34059  eldmres  34177  rnxrn  34296  rp-isfinite6  38181  undmrnresiss  38227  elintima  38262  pm11.58  38907  pm11.71  38914  2sbc5g  38934  iotasbc2  38938  ax6e2nd  39091  ax6e2ndVD  39458  ax6e2ndALT  39480  stoweidlem60  40595  elpglem3  42784