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 2353. (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  2573  2mo2  2647  reeanv  3209  cgsex2g  3475  cgsex4g  3476  spc2egv  3541  spc2ed  3543  dtruALT2  5312  exexneq  5387  copsex2t  5446  xpnz  6123  fununi  6573  frrlem4  8239  tfrlem7  8322  ener  8948  domtr  8954  unen  8992  undom  9003  sbthlem10  9034  mapen  9079  entrfil  9119  domtrfil  9126  sbthfilem  9132  infxpenc2  9944  fseqen  9949  dfac5lem4  10048  dfac5lem4OLD  10050  zorn2lem6  10423  fpwwe2lem11  10564  genpnnp  10928  hashfacen  14416  summo  15679  ntrivcvgmul  15867  prodmo  15901  iscatd2  17647  catcone0  17653  gictr  19251  gsumval3eu  19879  ptbasin  23542  txcls  23569  txbasval  23571  hmphtr  23748  reconn  24794  phtpcer  24962  pcohtpy  24987  mbfi1flimlem  25689  mbfmullem  25692  itg2add  25726  brabgaf  32679  pconnconn  35413  txsconn  35423  neibastop1  36541  bj-unexg  37345  cgsex2gd  37451  copsex2d  37453  riscer  38309  dmxrn  38708  disjecxrn  38733  br1cosscnvxrn  38885  dmqsblocks  39288  rictr  42965  fnchoice  45460  fzisoeu  45733  stoweidlem35  46463  elsprel  47935  grictr  48399