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 2379. (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  2599  2mo2  2673  reeanv  3235  cgsex2g  3496  cgsex4g  3497  spc2egv  3554  spc2ed  3556  dtruALT2  5332  exexneq  5403  copsex2t  5464  xpnz  6149  fununi  6607  frrlem4  8291  tfrlem7  8375  ener  9012  domtr  9018  unen  9057  undom  9068  sbthlem10  9099  mapen  9144  entrfil  9184  domtrfil  9191  sbthfilem  9197  infxpenc2  10082  fseqen  10087  dfac5lem4  10186  zorn2lem6  10560  fpwwe2lem11  10707  genpnnp  11071  hashfacen  14579  summo  15863  ntrivcvgmul  16051  prodmo  16083  iscatd2  17835  catcone0  17841  gictr  19470  gsumval3eu  20098  rictr  20732  ptbasin  23876  txcls  23903  txbasval  23905  hmphtr  24082  reconn  25128  phtpcer  25296  pcohtpy  25321  mbfi1flimlem  26023  mbfmullem  26026  itg2add  26060  brabgaf  33182  pconnconn  35965  txsconn  35975  neibastop1  37117  bj-unexg  37921  cgsex2gd  38026  copsex2d  38028  riscer  38890  dmxrn  39287  disjecxrn  39312  br1cosscnvxrn  39464  dmqsblocks  39867  fnchoice  45989  fzisoeu  46259  stoweidlem35  46989  elsprel  48501  grictr  48965