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 2351. (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  2573  2mo2  2647  reeanv  3229  cgsex2g  3527  cgsex4g  3528  cgsex4gOLD  3529  spc2egv  3599  spc2ed  3601  dtruALT2  5370  exexneq  5439  dtruOLD  5446  copsex2t  5497  xpnz  6179  fununi  6641  frrlem4  8314  wfrlem4OLD  8352  wfrfunOLD  8359  tfrlem7  8423  ener  9041  domtr  9047  unen  9086  undom  9099  undomOLD  9100  sbthlem10  9132  mapen  9181  entrfil  9225  domtrfil  9232  sbthfilem  9238  infxpenc2  10062  fseqen  10067  dfac5lem4  10166  dfac5lem4OLD  10168  zorn2lem6  10541  fpwwe2lem11  10681  genpnnp  11045  hashfacen  14493  summo  15753  ntrivcvgmul  15938  prodmo  15972  iscatd2  17724  catcone0  17730  gictr  19294  gsumval3eu  19922  ptbasin  23585  txcls  23612  txbasval  23614  hmphtr  23791  reconn  24850  phtpcer  25027  pcohtpy  25053  mbfi1flimlem  25757  mbfmullem  25760  itg2add  25794  brabgaf  32620  pconnconn  35236  txsconn  35246  neibastop1  36360  bj-unexg  37039  copsex2d  37140  riscer  37995  disjecxrn  38390  br1cosscnvxrn  38475  rictr  42530  fnchoice  45034  fzisoeu  45312  stoweidlem35  46050  elsprel  47462  grictr  47892