Theorem exdistrv 1952

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

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

This theorem is referenced by:  4exdistrv  1953  eu6lem  2570  2mo2  2644  reeanv  3226  cgsex2g  3524  cgsex4g  3525  cgsex4gOLD  3526  spc2egv  3598  spc2ed  3600  dtruALT2  5375  exexneq  5444  dtruOLD  5451  copsex2t  5502  xpnz  6180  fununi  6642  frrlem4  8312  wfrlem4OLD  8350  wfrfunOLD  8357  tfrlem7  8421  ener  9039  domtr  9045  unen  9084  undom  9097  undomOLD  9098  sbthlem10  9130  mapen  9179  entrfil  9222  domtrfil  9229  sbthfilem  9235  infxpenc2  10059  fseqen  10064  dfac5lem4  10163  dfac5lem4OLD  10165  zorn2lem6  10538  fpwwe2lem11  10678  genpnnp  11042  hashfacen  14489  summo  15749  ntrivcvgmul  15934  prodmo  15968  iscatd2  17725  catcone0  17731  gictr  19306  gsumval3eu  19936  ptbasin  23600  txcls  23627  txbasval  23629  hmphtr  23806  reconn  24863  phtpcer  25040  pcohtpy  25066  mbfi1flimlem  25771  mbfmullem  25774  itg2add  25808  brabgaf  32627  pconnconn  35215  txsconn  35225  neibastop1  36341  bj-unexg  37020  copsex2d  37121  riscer  37974  disjecxrn  38370  br1cosscnvxrn  38455  rictr  42506  fnchoice  44966  fzisoeu  45250  stoweidlem35  45990  elsprel  47399  grictr  47829