Theorem exdistrv 1990

Description: Distribute a pair of existential quantifiers (over disjoint variables) over a conjunction. Combination of 19.41v 1984 and 19.42v 1988. For a version with fewer disjoint variable conditions but requiring more axioms, see eeanv 2382. (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 1989	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.41v 1984	. 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 1945

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

This theorem is used by:  4exdistrv  1991  eu6lem  2601  2mo2  2675  reeanv  3238  cgsex2g  3499  cgsex4g  3500  spc2egv  3557  spc2ed  3559  dtruALT2  5337  exexneq  5408  copsex2t  5469  xpnz  6163  fununi  6640  frrlem4  8338  tfrlem7  8422  ener  9059  domtr  9065  unen  9104  undom  9115  sbthlem10  9146  mapen  9191  entrfil  9231  domtrfil  9238  sbthfilem  9244  infxpenc2  10131  fseqen  10136  dfac5lem4  10235  zorn2lem6  10609  fpwwe2lem11  10756  genpnnp  11120  hashfacen  14629  summo  15915  ntrivcvgmul  16103  prodmo  16135  iscatd2  17887  catcone0  17893  gictr  19523  gsumval3eu  20151  rictr  20785  ptbasin  23929  txcls  23956  txbasval  23958  hmphtr  24135  reconn  25181  phtpcer  25349  pcohtpy  25374  mbfi1flimlem  26076  mbfmullem  26079  itg2add  26113  brabgaf  33275  pconnconn  36176  txsconn  36186  neibastop1  37338  bj-unexg  38142  cgsex2gd  38263  copsex2d  38265  riscer  39125  dmxrn  39522  disjecxrn  39547  br1cosscnvxrn  39699  dmqsblocks  40102  fnchoice  46262  fzisoeu  46531  stoweidlem35  47260  elsprel  48772  grictr  49236