Theorem exdistrv 1988

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

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

This theorem is used by:  4exdistrv  1989  eu6lem  2600  2mo2  2674  reeanv  3236  cgsex2g  3498  cgsex4g  3499  spc2egv  3556  spc2ed  3558  dtruALT2  5339  exexneq  5414  copsex2t  5473  xpnz  6155  fununi  6612  frrlem4  8292  tfrlem7  8376  ener  9011  domtr  9017  unen  9056  undom  9067  sbthlem10  9098  mapen  9143  entrfil  9183  domtrfil  9190  sbthfilem  9196  infxpenc2  10029  fseqen  10034  dfac5lem4  10133  zorn2lem6  10507  fpwwe2lem11  10654  genpnnp  11018  hashfacen  14523  summo  15807  ntrivcvgmul  15995  prodmo  16029  iscatd2  17775  catcone0  17781  gictr  19409  gsumval3eu  20037  rictr  20669  ptbasin  23809  txcls  23836  txbasval  23838  hmphtr  24015  reconn  25061  phtpcer  25229  pcohtpy  25254  mbfi1flimlem  25956  mbfmullem  25959  itg2add  25993  brabgaf  33087  pconnconn  35818  txsconn  35828  neibastop1  36986  bj-unexg  37790  cgsex2gd  37897  copsex2d  37899  riscer  38746  dmxrn  39143  disjecxrn  39168  br1cosscnvxrn  39320  dmqsblocks  39723  fnchoice  45871  fzisoeu  46141  stoweidlem35  46871  elsprel  48383  grictr  48847