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 2350. (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  2572  2mo2  2646  reeanv  3213  cgsex2g  3506  cgsex4g  3507  cgsex4gOLD  3508  spc2egv  3578  spc2ed  3580  dtruALT2  5340  exexneq  5409  dtruOLD  5416  copsex2t  5467  xpnz  6148  fununi  6610  frrlem4  8286  wfrlem4OLD  8324  wfrfunOLD  8331  tfrlem7  8395  ener  9013  domtr  9019  unen  9058  undom  9071  undomOLD  9072  sbthlem10  9104  mapen  9153  entrfil  9197  domtrfil  9204  sbthfilem  9210  infxpenc2  10034  fseqen  10039  dfac5lem4  10138  dfac5lem4OLD  10140  zorn2lem6  10513  fpwwe2lem11  10653  genpnnp  11017  hashfacen  14470  summo  15731  ntrivcvgmul  15916  prodmo  15950  iscatd2  17691  catcone0  17697  gictr  19257  gsumval3eu  19883  ptbasin  23513  txcls  23540  txbasval  23542  hmphtr  23719  reconn  24766  phtpcer  24943  pcohtpy  24969  mbfi1flimlem  25673  mbfmullem  25676  itg2add  25710  brabgaf  32534  pconnconn  35199  txsconn  35209  neibastop1  36323  bj-unexg  37002  copsex2d  37103  riscer  37958  disjecxrn  38353  br1cosscnvxrn  38438  rictr  42490  fnchoice  45001  fzisoeu  45277  stoweidlem35  46012  elsprel  47437  grictr  47884