Theorem exdistrv 1957

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by:  4exdistrv  1958  eu6lem  2574  2mo2  2648  reeanv  3210  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  spc2egv  3555  spc2ed  3557  dtruALT2  5317  exexneq  5391  copsex2t  5448  xpnz  6125  fununi  6575  frrlem4  8241  tfrlem7  8324  ener  8950  domtr  8956  unen  8994  undom  9005  sbthlem10  9036  mapen  9081  entrfil  9121  domtrfil  9128  sbthfilem  9134  infxpenc2  9944  fseqen  9949  dfac5lem4  10048  dfac5lem4OLD  10050  zorn2lem6  10423  fpwwe2lem11  10564  genpnnp  10928  hashfacen  14389  summo  15652  ntrivcvgmul  15837  prodmo  15871  iscatd2  17616  catcone0  17622  gictr  19217  gsumval3eu  19845  ptbasin  23533  txcls  23560  txbasval  23562  hmphtr  23739  reconn  24785  phtpcer  24962  pcohtpy  24988  mbfi1flimlem  25691  mbfmullem  25694  itg2add  25728  brabgaf  32695  pconnconn  35444  txsconn  35454  neibastop1  36572  bj-unexg  37280  cgsex2gd  37386  copsex2d  37388  riscer  38233  dmxrn  38632  disjecxrn  38657  br1cosscnvxrn  38809  dmqsblocks  39212  rictr  42884  fnchoice  45383  fzisoeu  45656  stoweidlem35  46387  elsprel  47829  grictr  48277