Theorem exdistrv 1959

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

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  4exdistrv  1960  eu6lem  2567  2mo2  2643  reeanv  3226  cgsex2g  3519  cgsex4g  3520  cgsex4gOLD  3521  cgsex4gOLDOLD  3522  spc2egv  3589  spc2ed  3591  dtruALT2  5368  exexneq  5434  dtruOLD  5441  copsex2t  5492  copsex2gOLD  5494  xpnz  6158  fununi  6623  frrlem4  8273  wfrlem4OLD  8311  wfrfunOLD  8318  tfrlem7  8382  ener  8996  domtr  9002  unen  9045  undom  9058  undomOLD  9059  sbthlem10  9091  mapen  9140  entrfil  9187  domtrfil  9194  sbthfilem  9200  infxpenc2  10016  fseqen  10021  dfac5lem4  10120  zorn2lem6  10495  fpwwe2lem11  10635  genpnnp  10999  hashfacen  14412  hashfacenOLD  14413  summo  15662  ntrivcvgmul  15847  prodmo  15879  iscatd2  17624  catcone0  17630  gictr  19148  gsumval3eu  19771  ptbasin  23080  txcls  23107  txbasval  23109  hmphtr  23286  reconn  24343  phtpcer  24510  pcohtpy  24535  mbfi1flimlem  25239  mbfmullem  25242  itg2add  25276  brabgaf  31832  pconnconn  34217  txsconn  34227  neibastop1  35239  bj-unexg  35914  copsex2d  36015  riscer  36851  disjecxrn  37254  br1cosscnvxrn  37339  rictr  41097  fnchoice  43703  fzisoeu  44000  stoweidlem35  44741  elsprel  46133