Theorem exdistrv 1962

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

Syntax hints:   ↔ wb 207   ∧ wa 396  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787

This theorem is referenced by:  4exdistrv  1963  eu6lem  2577  2mo2  2651  reeanv  3212  cgsex2g  3478  cgsex4g  3479  spc2egv  3544  spc2ed  3546  dtruALT2  5306  exexneq  5381  copsex2t  5440  xpnz  6117  fununi  6567  frrlem4  8236  tfrlem7  8319  ener  8945  domtr  8951  unen  8989  undom  9000  sbthlem10  9031  mapen  9076  entrfil  9116  domtrfil  9123  sbthfilem  9129  infxpenc2  9942  fseqen  9947  dfac5lem4  10046  dfac5lem4OLD  10048  zorn2lem6  10421  fpwwe2lem11  10562  genpnnp  10926  hashfacen  14414  summo  15677  ntrivcvgmul  15865  prodmo  15899  iscatd2  17645  catcone0  17651  gictr  19249  gsumval3eu  19877  ptbasin  23567  txcls  23594  txbasval  23596  hmphtr  23773  reconn  24819  phtpcer  24987  pcohtpy  25012  mbfi1flimlem  25714  mbfmullem  25717  itg2add  25751  brabgaf  32705  pconnconn  35466  txsconn  35476  neibastop1  36594  bj-unexg  37398  cgsex2gd  37504  copsex2d  37506  riscer  38362  dmxrn  38761  disjecxrn  38786  br1cosscnvxrn  38938  dmqsblocks  39341  rictr  43013  fnchoice  45484  fzisoeu  45755  stoweidlem35  46485  elsprel  47957  grictr  48421