Theorem exdistrv 1955

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778

This theorem is referenced by:  4exdistrv  1956  eu6lem  2576  2mo2  2650  reeanv  3235  cgsex2g  3537  cgsex4g  3538  cgsex4gOLD  3539  spc2egv  3612  spc2ed  3614  dtruALT2  5388  exexneq  5454  dtruOLD  5461  copsex2t  5512  xpnz  6190  fununi  6653  frrlem4  8330  wfrlem4OLD  8368  wfrfunOLD  8375  tfrlem7  8439  ener  9061  domtr  9067  unen  9112  undom  9125  undomOLD  9126  sbthlem10  9158  mapen  9207  entrfil  9251  domtrfil  9258  sbthfilem  9264  infxpenc2  10091  fseqen  10096  dfac5lem4  10195  dfac5lem4OLD  10197  zorn2lem6  10570  fpwwe2lem11  10710  genpnnp  11074  hashfacen  14503  summo  15765  ntrivcvgmul  15950  prodmo  15984  iscatd2  17739  catcone0  17745  gictr  19316  gsumval3eu  19946  ptbasin  23606  txcls  23633  txbasval  23635  hmphtr  23812  reconn  24869  phtpcer  25046  pcohtpy  25072  mbfi1flimlem  25777  mbfmullem  25780  itg2add  25814  brabgaf  32630  pconnconn  35199  txsconn  35209  neibastop1  36325  bj-unexg  37004  copsex2d  37105  riscer  37948  disjecxrn  38345  br1cosscnvxrn  38430  rictr  42475  fnchoice  44929  fzisoeu  45215  stoweidlem35  45956  elsprel  47349  grictr  47776