Theorem exdistrv 1956

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

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781

This theorem is referenced by:  4exdistrv  1957  eu6lem  2658  2mo2  2732  reeanv  3367  cgsex2g  3538  cgsex4g  3539  vtocl2OLD  3562  spc2egv  3600  spc2ed  3602  dtru  5271  copsex2t  5383  copsex2g  5384  xpnz  6016  fununi  6429  wfrlem4  7958  wfrfun  7965  tfrlem7  8019  ener  8556  domtr  8562  unen  8596  undom  8605  sbthlem10  8636  mapen  8681  infxpenc2  9448  fseqen  9453  dfac5lem4  9552  zorn2lem6  9923  fpwwe2lem12  10063  genpnnp  10427  hashfacen  13813  summo  15074  ntrivcvgmul  15258  prodmo  15290  iscatd2  16952  gictr  18415  gsumval3eu  19024  ptbasin  22185  txcls  22212  txbasval  22214  hmphtr  22391  reconn  23436  phtpcer  23599  pcohtpy  23624  mbfi1flimlem  24323  mbfmullem  24326  itg2add  24360  brabgaf  30359  pconnconn  32478  txsconn  32488  frrlem4  33126  neibastop1  33707  bj-dtru  34139  copsex2d  34434  riscer  35281  br1cosscnvxrn  35729  sn-dtru  39160  fnchoice  41335  fzisoeu  41616  stoweidlem35  42369  elsprel  43686