Theorem exdistrv 1998

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

Syntax hints:   ↔ wb 198   ∧ wa 386  ∃wex 1823

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

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824

This theorem is referenced by:  4exdistrv  1999  eu6lem  2591  eu6OLD  2594  2mo2  2677  cgsex2g  3441  cgsex4g  3442  vtocl2  3462  spc2egv  3497  dtru  5084  copsex2t  5190  copsex2g  5191  xpnz  5809  fununi  6211  wfrlem4  7702  wfrfun  7710  tfrlem7  7764  ener  8290  domtr  8296  unen  8330  undom  8338  sbthlem10  8369  mapen  8414  infxpenc2  9180  fseqen  9185  dfac5lem4  9284  zorn2lem6  9660  fpwwe2lem12  9800  genpnnp  10164  hashfacen  13556  summo  14859  ntrivcvgmul  15041  prodmo  15073  iscatd2  16731  gictr  18105  gsumval3eu  18695  ptbasin  21793  txcls  21820  txbasval  21822  hmphtr  21999  reconn  23043  phtpcer  23206  pcohtpy  23231  mbfi1flimlem  23930  mbfmullem  23933  itg2add  23967  spc2ed  29888  brabgaf  29987  pconnconn  31816  txsconn  31826  frrlem4  32376  frrlem5c  32379  neibastop1  32946  bj-dtru  33377  riscer  34416  br1cosscnvxrn  34857  fnchoice  40131  fzisoeu  40433  stoweidlem35  41189  elsprel  42424