Theorem exdistrv 1978

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

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803

This theorem is referenced by:  4exdistrv  1979  eu6lem  2603  2mo2  2677  reeanv  3237  cgsex2g  3502  cgsex4g  3503  spc2egv  3561  spc2ed  3563  dtruALT2  5332  exexneq  5407  copsex2t  5466  xpnz  6148  fununi  6600  frrlem4  8274  tfrlem7  8358  ener  8986  domtr  8992  unen  9030  undom  9041  sbthlem10  9072  mapen  9117  entrfil  9157  domtrfil  9164  sbthfilem  9170  infxpenc2  9994  fseqen  9999  dfac5lem4  10098  zorn2lem6  10473  fpwwe2lem11  10614  genpnnp  10978  hashfacen  14481  summo  15758  ntrivcvgmul  15946  prodmo  15980  iscatd2  17727  catcone0  17733  gictr  19337  gsumval3eu  19965  ptbasin  23695  txcls  23722  txbasval  23724  hmphtr  23901  reconn  24947  phtpcer  25115  pcohtpy  25140  mbfi1flimlem  25842  mbfmullem  25845  itg2add  25879  brabgaf  32863  pconnconn  35594  txsconn  35604  neibastop1  36732  bj-unexg  37535  cgsex2gd  37641  copsex2d  37643  riscer  38499  dmxrn  38898  disjecxrn  38923  br1cosscnvxrn  39075  dmqsblocks  39478  rictr  43150  fnchoice  45607  fzisoeu  45877  stoweidlem35  46607  elsprel  48079  grictr  48543