Theorem exdistrv 1960

Description: Distribute a pair of existential quantifiers (over disjoint variables) over a conjunction. Combination of 19.41v 1954 and 19.42v 1958. For a version with fewer disjoint variable conditions but requiring more axioms, see eeanv 2349. (Contributed by BJ, 30-Sep-2022.)

Assertion

Ref	Expression
exdistrv	⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))

Distinct variable groups:   𝜑,𝑦   𝜓,𝑥   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem exdistrv

Step	Hyp	Ref	Expression
1		exdistr 1959	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.41v 1954	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
3	1, 2	bitri 274	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 395  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784

This theorem is referenced by:  4exdistrv  1961  eu6lem  2573  2mo2  2649  reeanv  3292  cgsex2g  3465  cgsex4g  3466  cgsex4gOLD  3467  spc2egv  3528  spc2ed  3530  dtru  5288  copsex2t  5400  copsex2gOLD  5402  xpnz  6051  fununi  6493  frrlem4  8076  wfrlem4OLD  8114  wfrfunOLD  8121  tfrlem7  8185  ener  8742  domtr  8748  unen  8790  undom  8800  sbthlem10  8832  mapen  8877  entrfil  8931  domtrfi  8938  sbthfilem  8941  infxpenc2  9709  fseqen  9714  dfac5lem4  9813  zorn2lem6  10188  fpwwe2lem11  10328  genpnnp  10692  hashfacen  14094  hashfacenOLD  14095  summo  15357  ntrivcvgmul  15542  prodmo  15574  iscatd2  17307  catcone0  17313  gictr  18806  gsumval3eu  19420  ptbasin  22636  txcls  22663  txbasval  22665  hmphtr  22842  reconn  23897  phtpcer  24064  pcohtpy  24089  mbfi1flimlem  24792  mbfmullem  24795  itg2add  24829  brabgaf  30849  pconnconn  33093  txsconn  33103  neibastop1  34475  bj-dtru  34926  copsex2d  35237  riscer  36073  br1cosscnvxrn  36519  sn-dtru  40116  fnchoice  42461  fzisoeu  42729  stoweidlem35  43466  elsprel  44815