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 2347. (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 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

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

This theorem is referenced by:  4exdistrv  1960  eu6lem  2573  2mo2  2649  reeanv  3294  cgsex2g  3475  cgsex4g  3476  cgsex4gOLD  3477  spc2egv  3538  spc2ed  3540  dtruALT2  5293  dtru  5359  copsex2t  5406  copsex2gOLD  5408  xpnz  6062  fununi  6509  frrlem4  8105  wfrlem4OLD  8143  wfrfunOLD  8150  tfrlem7  8214  ener  8787  domtr  8793  unen  8836  undom  8846  undomOLD  8847  sbthlem10  8879  mapen  8928  entrfil  8971  domtrfil  8978  sbthfilem  8984  infxpenc2  9778  fseqen  9783  dfac5lem4  9882  zorn2lem6  10257  fpwwe2lem11  10397  genpnnp  10761  hashfacen  14166  hashfacenOLD  14167  summo  15429  ntrivcvgmul  15614  prodmo  15646  iscatd2  17390  catcone0  17396  gictr  18891  gsumval3eu  19505  ptbasin  22728  txcls  22755  txbasval  22757  hmphtr  22934  reconn  23991  phtpcer  24158  pcohtpy  24183  mbfi1flimlem  24887  mbfmullem  24890  itg2add  24924  brabgaf  30948  pconnconn  33193  txsconn  33203  neibastop1  34548  bj-dtru  34999  copsex2d  35310  riscer  36146  br1cosscnvxrn  36592  sn-dtru  40188  fnchoice  42572  fzisoeu  42839  stoweidlem35  43576  elsprel  44927