Theorem exdistrv 1987

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  4exdistrv  1988  eu6lem  2598  2mo2  2672  reeanv  3234  cgsex2g  3495  cgsex4g  3496  spc2egv  3553  spc2ed  3555  dtruALT2  5331  exexneq  5402  copsex2t  5463  xpnz  6149  fununi  6615  frrlem4  8310  tfrlem7  8394  ener  9031  domtr  9037  unen  9076  undom  9087  sbthlem10  9118  mapen  9163  entrfil  9203  domtrfil  9210  sbthfilem  9216  infxpenc2  10104  fseqen  10109  dfac5lem4  10208  zorn2lem6  10582  fpwwe2lem11  10729  genpnnp  11093  hashfacen  14602  summo  15888  ntrivcvgmul  16076  prodmo  16108  iscatd2  17860  catcone0  17866  gictr  19495  gsumval3eu  20123  rictr  20757  ptbasin  23901  txcls  23928  txbasval  23930  hmphtr  24107  reconn  25153  phtpcer  25321  pcohtpy  25346  mbfi1flimlem  26048  mbfmullem  26051  itg2add  26085  brabgaf  33247  pconnconn  36082  txsconn  36092  neibastop1  37239  bj-unexg  38043  cgsex2gd  38151  copsex2d  38153  riscer  39015  dmxrn  39412  disjecxrn  39437  br1cosscnvxrn  39589  dmqsblocks  39992  fnchoice  46139  fzisoeu  46409  stoweidlem35  47138  elsprel  48650  grictr  49114