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 2351. (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  2570  2mo2  2644  reeanv  3205  cgsex2g  3483  cgsex4g  3484  cgsex4gOLD  3485  spc2egv  3550  spc2ed  3552  dtruALT2  5310  exexneq  5379  copsex2t  5435  xpnz  6111  fununi  6561  frrlem4  8225  tfrlem7  8308  ener  8930  domtr  8936  unen  8974  undom  8985  sbthlem10  9016  mapen  9061  entrfil  9101  domtrfil  9108  sbthfilem  9114  infxpenc2  9920  fseqen  9925  dfac5lem4  10024  dfac5lem4OLD  10026  zorn2lem6  10399  fpwwe2lem11  10539  genpnnp  10903  hashfacen  14363  summo  15626  ntrivcvgmul  15811  prodmo  15845  iscatd2  17589  catcone0  17595  gictr  19190  gsumval3eu  19818  ptbasin  23493  txcls  23520  txbasval  23522  hmphtr  23699  reconn  24745  phtpcer  24922  pcohtpy  24948  mbfi1flimlem  25651  mbfmullem  25654  itg2add  25688  brabgaf  32591  pconnconn  35296  txsconn  35306  neibastop1  36424  bj-unexg  37103  copsex2d  37204  riscer  38048  dmxrn  38431  disjecxrn  38456  br1cosscnvxrn  38596  dmqsblocks  38971  rictr  42638  fnchoice  45150  fzisoeu  45425  stoweidlem35  46157  elsprel  47599  grictr  48047