Theorem 19.42vv 1962

Description: Version of 19.42 2230 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 275	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 397  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783

This theorem is referenced by:  exdistr2  1963  3exdistr  1965  cgsex4g  3521  ceqsex3v  3532  ceqsex4v  3533  ceqsex8v  3535  elvvv  5752  xpdifid  6168  dfoprab2  7467  resoprab  7526  elrnmpores  7546  ov3  7570  ov6g  7571  oprabex3  7964  xpassen  9066  entrfil  9188  domtrfil  9195  sbthfilem  9201  axaddf  11140  axmulf  11141  catcone0  17631  qqhval2  32962  bnj996  33967  fineqvac  34097  inxpxrn  37265  dvhopellsm  39988