Theorem 19.42vv 1964

Description: Version of 19.42 2248 with two quantifiers and a disjoint variable condition requiring fewer axioms. (Contributed by NM, 16-Mar-1995.)

Assertion

Ref	Expression
19.42vv	⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)

Proof of Theorem 19.42vv

Step	Hyp	Ref	Expression
1		exdistr 1961	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.42v 1960	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))
3	1, 2	bitri 276	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))

Syntax hints:   ↔ wb 207   ∧ wa 396  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787

This theorem is referenced by:  exdistr2  1965  3exdistr  1967  cgsex4g  3477  ceqsex3v  3484  ceqsex4v  3485  ceqsex8v  3487  elvvv  5694  xpdifid  6119  dfoprab2  7414  resoprab  7474  elrnmpores  7494  ov3  7519  ov6g  7520  oprabex3  7919  xpassen  8999  entrfil  9109  domtrfil  9116  sbthfilem  9122  axaddf  11059  axmulf  11060  catcone0  17644  qqhval2  34166  bnj996  35138  fineqvac  35297  inxpxrn  38785  dmqsblocks  39334  dvhopellsm  41609