Theorem exdistrv 1956

Description: Distribute a pair of existential quantifiers (over disjoint variables) over a conjunction. Combination of 19.41v 1950 and 19.42v 1954. 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 1955	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.41v 1950	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
3	1, 2	bitri 275	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  4exdistrv  1957  eu6lem  2568  2mo2  2642  reeanv  3204  cgsex2g  3482  cgsex4g  3483  cgsex4gOLD  3484  spc2egv  3554  spc2ed  3556  dtruALT2  5308  exexneq  5377  copsex2t  5432  xpnz  6106  fununi  6556  frrlem4  8219  tfrlem7  8302  ener  8923  domtr  8929  unen  8967  undom  8978  sbthlem10  9009  mapen  9054  entrfil  9094  domtrfil  9101  sbthfilem  9107  infxpenc2  9910  fseqen  9915  dfac5lem4  10014  dfac5lem4OLD  10016  zorn2lem6  10389  fpwwe2lem11  10529  genpnnp  10893  hashfacen  14358  summo  15621  ntrivcvgmul  15806  prodmo  15840  iscatd2  17584  catcone0  17590  gictr  19186  gsumval3eu  19814  ptbasin  23490  txcls  23517  txbasval  23519  hmphtr  23696  reconn  24742  phtpcer  24919  pcohtpy  24945  mbfi1flimlem  25648  mbfmullem  25651  itg2add  25685  brabgaf  32584  pconnconn  35263  txsconn  35273  neibastop1  36392  bj-unexg  37071  copsex2d  37172  riscer  38027  dmxrn  38405  disjecxrn  38420  br1cosscnvxrn  38510  dmqsblocks  38890  rictr  42552  fnchoice  45065  fzisoeu  45340  stoweidlem35  46072  elsprel  47505  grictr  47953