Theorem exdistrv 1988

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  4exdistrv  1989  eu6lem  2604  2mo2  2678  reeanv  3240  cgsex2g  3503  cgsex4g  3504  spc2egv  3561  spc2ed  3563  dtruALT2  5346  exexneq  5421  copsex2t  5480  xpnz  6161  fununi  6618  frrlem4  8295  tfrlem7  8379  ener  9007  domtr  9013  unen  9052  undom  9063  sbthlem10  9094  mapen  9139  entrfil  9179  domtrfil  9186  sbthfilem  9192  infxpenc2  10025  fseqen  10030  dfac5lem4  10129  zorn2lem6  10503  fpwwe2lem11  10644  genpnnp  11008  hashfacen  14511  summo  15794  ntrivcvgmul  15982  prodmo  16016  iscatd2  17762  catcone0  17768  gictr  19377  gsumval3eu  20005  rictr  20637  ptbasin  23771  txcls  23798  txbasval  23800  hmphtr  23977  reconn  25023  phtpcer  25191  pcohtpy  25216  mbfi1flimlem  25918  mbfmullem  25921  itg2add  25955  brabgaf  32988  pconnconn  35744  txsconn  35754  neibastop1  36911  bj-unexg  37715  cgsex2gd  37822  copsex2d  37824  riscer  38680  dmxrn  39077  disjecxrn  39102  br1cosscnvxrn  39254  dmqsblocks  39657  fnchoice  45790  fzisoeu  46060  stoweidlem35  46790  elsprel  48265  grictr  48729