Theorem exdistrv 1957

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃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 1912

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

This theorem is referenced by:  4exdistrv  1958  eu6lem  2574  2mo2  2648  reeanv  3210  cgsex2g  3476  cgsex4g  3477  spc2egv  3542  spc2ed  3544  dtruALT2  5305  exexneq  5380  copsex2t  5438  xpnz  6115  fununi  6565  frrlem4  8230  tfrlem7  8313  ener  8939  domtr  8945  unen  8983  undom  8994  sbthlem10  9025  mapen  9070  entrfil  9110  domtrfil  9117  sbthfilem  9123  infxpenc2  9933  fseqen  9938  dfac5lem4  10037  dfac5lem4OLD  10039  zorn2lem6  10412  fpwwe2lem11  10553  genpnnp  10917  hashfacen  14405  summo  15668  ntrivcvgmul  15856  prodmo  15890  iscatd2  17636  catcone0  17642  gictr  19240  gsumval3eu  19868  ptbasin  23551  txcls  23578  txbasval  23580  hmphtr  23757  reconn  24803  phtpcer  24971  pcohtpy  24996  mbfi1flimlem  25698  mbfmullem  25701  itg2add  25735  brabgaf  32699  pconnconn  35434  txsconn  35444  neibastop1  36562  bj-unexg  37358  cgsex2gd  37464  copsex2d  37466  riscer  38320  dmxrn  38719  disjecxrn  38744  br1cosscnvxrn  38896  dmqsblocks  39299  rictr  42976  fnchoice  45475  fzisoeu  45748  stoweidlem35  46478  elsprel  47932  grictr  48396