Theorem exdistrv 1956

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  4exdistrv  1957  eu6lem  2573  2mo2  2647  reeanv  3208  cgsex2g  3486  cgsex4g  3487  cgsex4gOLD  3488  spc2egv  3553  spc2ed  3555  dtruALT2  5315  exexneq  5384  copsex2t  5440  xpnz  6117  fununi  6567  frrlem4  8231  tfrlem7  8314  ener  8938  domtr  8944  unen  8982  undom  8993  sbthlem10  9024  mapen  9069  entrfil  9109  domtrfil  9116  sbthfilem  9122  infxpenc2  9932  fseqen  9937  dfac5lem4  10036  dfac5lem4OLD  10038  zorn2lem6  10411  fpwwe2lem11  10552  genpnnp  10916  hashfacen  14377  summo  15640  ntrivcvgmul  15825  prodmo  15859  iscatd2  17604  catcone0  17610  gictr  19205  gsumval3eu  19833  ptbasin  23521  txcls  23548  txbasval  23550  hmphtr  23727  reconn  24773  phtpcer  24950  pcohtpy  24976  mbfi1flimlem  25679  mbfmullem  25682  itg2add  25716  brabgaf  32684  pconnconn  35425  txsconn  35435  neibastop1  36553  bj-unexg  37239  copsex2d  37340  riscer  38185  dmxrn  38568  disjecxrn  38593  br1cosscnvxrn  38733  dmqsblocks  39108  rictr  42771  fnchoice  45270  fzisoeu  45544  stoweidlem35  46275  elsprel  47717  grictr  48165