Theorem exdistrv 1959

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

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  4exdistrv  1960  eu6lem  2567  2mo2  2643  reeanv  3226  cgsex2g  3519  cgsex4g  3520  cgsex4gOLD  3521  cgsex4gOLDOLD  3522  spc2egv  3589  spc2ed  3591  dtruALT2  5368  exexneq  5434  dtruOLD  5441  copsex2t  5492  copsex2gOLD  5494  xpnz  6158  fununi  6623  frrlem4  8276  wfrlem4OLD  8314  wfrfunOLD  8321  tfrlem7  8385  ener  8999  domtr  9005  unen  9048  undom  9061  undomOLD  9062  sbthlem10  9094  mapen  9143  entrfil  9190  domtrfil  9197  sbthfilem  9203  infxpenc2  10019  fseqen  10024  dfac5lem4  10123  zorn2lem6  10498  fpwwe2lem11  10638  genpnnp  11002  hashfacen  14415  hashfacenOLD  14416  summo  15665  ntrivcvgmul  15850  prodmo  15882  iscatd2  17627  catcone0  17633  gictr  19151  gsumval3eu  19774  ptbasin  23088  txcls  23115  txbasval  23117  hmphtr  23294  reconn  24351  phtpcer  24518  pcohtpy  24543  mbfi1flimlem  25247  mbfmullem  25250  itg2add  25284  brabgaf  31875  pconnconn  34291  txsconn  34301  neibastop1  35330  bj-unexg  36005  copsex2d  36106  riscer  36942  disjecxrn  37345  br1cosscnvxrn  37430  rictr  41179  fnchoice  43795  fzisoeu  44089  stoweidlem35  44830  elsprel  46222