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  2566  2mo2  2640  reeanv  3201  cgsex2g  3484  cgsex4g  3485  cgsex4gOLD  3486  spc2egv  3556  spc2ed  3558  dtruALT2  5312  exexneq  5381  dtruOLD  5388  copsex2t  5439  xpnz  6112  fununi  6561  frrlem4  8229  tfrlem7  8312  ener  8933  domtr  8939  unen  8978  undom  8989  sbthlem10  9020  mapen  9065  entrfil  9109  domtrfil  9116  sbthfilem  9122  infxpenc2  9935  fseqen  9940  dfac5lem4  10039  dfac5lem4OLD  10041  zorn2lem6  10414  fpwwe2lem11  10554  genpnnp  10918  hashfacen  14379  summo  15642  ntrivcvgmul  15827  prodmo  15861  iscatd2  17605  catcone0  17611  gictr  19173  gsumval3eu  19801  ptbasin  23480  txcls  23507  txbasval  23509  hmphtr  23686  reconn  24733  phtpcer  24910  pcohtpy  24936  mbfi1flimlem  25639  mbfmullem  25642  itg2add  25676  brabgaf  32569  pconnconn  35203  txsconn  35213  neibastop1  36332  bj-unexg  37011  copsex2d  37112  riscer  37967  dmxrn  38345  disjecxrn  38360  br1cosscnvxrn  38450  dmqsblocks  38830  rictr  42493  fnchoice  45007  fzisoeu  45282  stoweidlem35  46017  elsprel  47460  grictr  47908