Theorem exdistrv 1974

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

Syntax hints:   ↔ wb 208   ∧ wa 399  ∃wex 1798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799

This theorem is referenced by:  4exdistrv  1975  eu6lem  2599  2mo2  2673  reeanv  3233  cgsex2g  3498  cgsex4g  3499  spc2egv  3558  spc2ed  3560  dtruALT2  5326  exexneq  5401  copsex2t  5460  xpnz  6141  fununi  6592  frrlem4  8265  tfrlem7  8349  ener  8978  domtr  8984  unen  9022  undom  9033  sbthlem10  9064  mapen  9109  entrfil  9149  domtrfil  9156  sbthfilem  9162  infxpenc2  9975  fseqen  9980  dfac5lem4  10079  dfac5lem4OLD  10081  zorn2lem6  10455  fpwwe2lem11  10596  genpnnp  10960  hashfacen  14464  summo  15727  ntrivcvgmul  15915  prodmo  15949  iscatd2  17696  catcone0  17702  gictr  19299  gsumval3eu  19927  ptbasin  23617  txcls  23644  txbasval  23646  hmphtr  23823  reconn  24869  phtpcer  25037  pcohtpy  25062  mbfi1flimlem  25764  mbfmullem  25767  itg2add  25801  brabgaf  32758  pconnconn  35545  txsconn  35555  neibastop1  36683  bj-unexg  37487  cgsex2gd  37593  copsex2d  37595  riscer  38451  dmxrn  38850  disjecxrn  38875  br1cosscnvxrn  39027  dmqsblocks  39430  rictr  43102  fnchoice  45573  fzisoeu  45843  stoweidlem35  46573  elsprel  48045  grictr  48509