Theorem exdistrv 1955

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

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780

This theorem is referenced by:  4exdistrv  1956  eu6lem  2657  2mo2  2731  reeanv  3370  cgsex2g  3541  cgsex4g  3542  vtocl2OLD  3565  spc2egv  3603  spc2ed  3605  dtru  5274  copsex2t  5386  copsex2g  5387  xpnz  6019  fununi  6432  wfrlem4  7961  wfrfun  7968  tfrlem7  8022  ener  8559  domtr  8565  unen  8599  undom  8608  sbthlem10  8639  mapen  8684  infxpenc2  9451  fseqen  9456  dfac5lem4  9555  zorn2lem6  9926  fpwwe2lem12  10066  genpnnp  10430  hashfacen  13815  summo  15077  ntrivcvgmul  15261  prodmo  15293  iscatd2  16955  gictr  18418  gsumval3eu  19027  ptbasin  22188  txcls  22215  txbasval  22217  hmphtr  22394  reconn  23439  phtpcer  23602  pcohtpy  23627  mbfi1flimlem  24326  mbfmullem  24329  itg2add  24363  brabgaf  30362  pconnconn  32482  txsconn  32492  frrlem4  33130  neibastop1  33711  bj-dtru  34143  copsex2d  34435  riscer  35270  br1cosscnvxrn  35718  sn-dtru  39117  fnchoice  41292  fzisoeu  41573  stoweidlem35  42327  elsprel  43644