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 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 1954	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.41v 1949	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
3	1, 2	bitri 275	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃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 207  df-an 396  df-ex 1780

This theorem is referenced by:  4exdistrv  1956  eu6lem  2567  2mo2  2641  reeanv  3210  cgsex2g  3496  cgsex4g  3497  cgsex4gOLD  3498  spc2egv  3568  spc2ed  3570  dtruALT2  5328  exexneq  5397  dtruOLD  5404  copsex2t  5455  xpnz  6135  fununi  6594  frrlem4  8271  tfrlem7  8354  ener  8975  domtr  8981  unen  9020  undom  9033  undomOLD  9034  sbthlem10  9066  mapen  9111  entrfil  9155  domtrfil  9162  sbthfilem  9168  infxpenc2  9982  fseqen  9987  dfac5lem4  10086  dfac5lem4OLD  10088  zorn2lem6  10461  fpwwe2lem11  10601  genpnnp  10965  hashfacen  14426  summo  15690  ntrivcvgmul  15875  prodmo  15909  iscatd2  17649  catcone0  17655  gictr  19215  gsumval3eu  19841  ptbasin  23471  txcls  23498  txbasval  23500  hmphtr  23677  reconn  24724  phtpcer  24901  pcohtpy  24927  mbfi1flimlem  25630  mbfmullem  25633  itg2add  25667  brabgaf  32543  pconnconn  35225  txsconn  35235  neibastop1  36354  bj-unexg  37033  copsex2d  37134  riscer  37989  dmxrn  38367  disjecxrn  38382  br1cosscnvxrn  38472  dmqsblocks  38852  rictr  42515  fnchoice  45030  fzisoeu  45305  stoweidlem35  46040  elsprel  47480  grictr  47927