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 2359. (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 278	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1781

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782

This theorem is referenced by:  4exdistrv  1957  eu6lem  2633  2mo2  2709  reeanv  3320  cgsex2g  3485  cgsex4g  3486  cgsex4gOLD  3487  vtocl2OLD  3510  spc2egv  3548  spc2ed  3550  dtru  5236  copsex2t  5348  copsex2g  5349  xpnz  5983  fununi  6399  wfrlem4  7941  wfrfun  7948  tfrlem7  8002  ener  8539  domtr  8545  unen  8579  undom  8588  sbthlem10  8620  mapen  8665  infxpenc2  9433  fseqen  9438  dfac5lem4  9537  zorn2lem6  9912  fpwwe2lem12  10052  genpnnp  10416  hashfacen  13808  summo  15066  ntrivcvgmul  15250  prodmo  15282  iscatd2  16944  gictr  18407  gsumval3eu  19017  ptbasin  22182  txcls  22209  txbasval  22211  hmphtr  22388  reconn  23433  phtpcer  23600  pcohtpy  23625  mbfi1flimlem  24326  mbfmullem  24329  itg2add  24363  brabgaf  30372  pconnconn  32591  txsconn  32601  frrlem4  33239  neibastop1  33820  bj-dtru  34254  copsex2d  34554  riscer  35426  br1cosscnvxrn  35874  sn-dtru  39403  fnchoice  41658  fzisoeu  41932  stoweidlem35  42677  elsprel  43992