Theorem exdistrv 1957

Description: Distribute a pair of existential quantifiers (over disjoint variables) over a conjunction. Combination of 19.41v 1951 and 19.42v 1955. For a version with fewer disjoint variable conditions but requiring more axioms, see eeanv 2354. (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 1956	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.41v 1951	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
3	1, 2	bitri 275	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by:  4exdistrv  1958  eu6lem  2574  2mo2  2648  reeanv  3210  cgsex2g  3476  cgsex4g  3477  spc2egv  3542  spc2ed  3544  dtruALT2  5307  exexneq  5382  copsex2t  5440  xpnz  6117  fununi  6567  frrlem4  8232  tfrlem7  8315  ener  8941  domtr  8947  unen  8985  undom  8996  sbthlem10  9027  mapen  9072  entrfil  9112  domtrfil  9119  sbthfilem  9125  infxpenc2  9935  fseqen  9940  dfac5lem4  10039  dfac5lem4OLD  10041  zorn2lem6  10414  fpwwe2lem11  10555  genpnnp  10919  hashfacen  14407  summo  15670  ntrivcvgmul  15858  prodmo  15892  iscatd2  17638  catcone0  17644  gictr  19242  gsumval3eu  19870  ptbasin  23552  txcls  23579  txbasval  23581  hmphtr  23758  reconn  24804  phtpcer  24972  pcohtpy  24997  mbfi1flimlem  25699  mbfmullem  25702  itg2add  25736  brabgaf  32694  pconnconn  35429  txsconn  35439  neibastop1  36557  bj-unexg  37361  cgsex2gd  37467  copsex2d  37469  riscer  38323  dmxrn  38722  disjecxrn  38747  br1cosscnvxrn  38899  dmqsblocks  39302  rictr  42979  fnchoice  45478  fzisoeu  45751  stoweidlem35  46481  elsprel  47947  grictr  48411