Theorem exdistrv 1985

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

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

This theorem is referenced by:  4exdistrv  1986  eu6lem  2601  2mo2  2675  reeanv  3237  cgsex2g  3500  cgsex4g  3501  spc2egv  3559  spc2ed  3561  dtruALT2  5343  exexneq  5418  copsex2t  5477  xpnz  6158  fununi  6613  frrlem4  8287  tfrlem7  8371  ener  8999  domtr  9005  unen  9043  undom  9054  sbthlem10  9085  mapen  9130  entrfil  9170  domtrfil  9177  sbthfilem  9183  infxpenc2  10007  fseqen  10012  dfac5lem4  10111  zorn2lem6  10486  fpwwe2lem11  10627  genpnnp  10991  hashfacen  14493  summo  15770  ntrivcvgmul  15958  prodmo  15992  iscatd2  17738  catcone0  17744  gictr  19347  gsumval3eu  19975  ptbasin  23715  txcls  23742  txbasval  23744  hmphtr  23921  reconn  24967  phtpcer  25135  pcohtpy  25160  mbfi1flimlem  25862  mbfmullem  25865  itg2add  25899  brabgaf  32929  pconnconn  35701  txsconn  35711  neibastop1  36848  bj-unexg  37652  cgsex2gd  37759  copsex2d  37761  riscer  38617  dmxrn  39014  disjecxrn  39039  br1cosscnvxrn  39191  dmqsblocks  39594  rictr  43268  fnchoice  45729  fzisoeu  45999  stoweidlem35  46729  elsprel  48201  grictr  48665