Theorem exdistrv 1955

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  4exdistrv  1956  eu6lem  2566  2mo2  2640  reeanv  3209  cgsex2g  3493  cgsex4g  3494  cgsex4gOLD  3495  spc2egv  3565  spc2ed  3567  dtruALT2  5325  exexneq  5394  dtruOLD  5401  copsex2t  5452  xpnz  6132  fununi  6591  frrlem4  8268  tfrlem7  8351  ener  8972  domtr  8978  unen  9017  undom  9029  sbthlem10  9060  mapen  9105  entrfil  9149  domtrfil  9156  sbthfilem  9162  infxpenc2  9975  fseqen  9980  dfac5lem4  10079  dfac5lem4OLD  10081  zorn2lem6  10454  fpwwe2lem11  10594  genpnnp  10958  hashfacen  14419  summo  15683  ntrivcvgmul  15868  prodmo  15902  iscatd2  17642  catcone0  17648  gictr  19208  gsumval3eu  19834  ptbasin  23464  txcls  23491  txbasval  23493  hmphtr  23670  reconn  24717  phtpcer  24894  pcohtpy  24920  mbfi1flimlem  25623  mbfmullem  25626  itg2add  25660  brabgaf  32536  pconnconn  35218  txsconn  35228  neibastop1  36347  bj-unexg  37026  copsex2d  37127  riscer  37982  dmxrn  38360  disjecxrn  38375  br1cosscnvxrn  38465  dmqsblocks  38845  rictr  42508  fnchoice  45023  fzisoeu  45298  stoweidlem35  46033  elsprel  47476  grictr  47923