Theorem 19.42vv 1962

Description: Version of 19.42 2232 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 1959	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.42v 1958	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))
3	1, 2	bitri 274	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 395  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784

This theorem is referenced by:  exdistr2  1963  3exdistr  1965  ceqsex3v  3474  ceqsex4v  3475  ceqsex8v  3477  elvvv  5653  xpdifid  6060  dfoprab2  7311  resoprab  7370  elrnmpores  7389  ov3  7413  ov6g  7414  oprabex3  7793  xpassen  8806  entrfil  8931  domtrfi  8938  sbthfilem  8941  axaddf  10832  axmulf  10833  catcone0  17313  qqhval2  31832  bnj996  32836  fineqvac  32966  inxpxrn  36448  dvhopellsm  39058