Theorem 19.42vv 1907

Description: Version of 19.42 2092 with two quantifiers and a dv 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 1906	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.42v 1905	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))
3	1, 2	bitri 263	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))

Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696

This theorem is referenced by:  19.42vvv  1908  exdistr2  1909  3exdistr  1910  ceqsex3v  3219  ceqsex4v  3220  ceqsex8v  3222  elvvv  5101  xpdifid  5481  dfoprab2  6599  resoprab  6654  elrnmpt2res  6672  ov3  6695  ov6g  6696  oprabex3  7048  xpassen  7939  axaddf  9845  axmulf  9846  usgraedg4  25916  el2wlkonot  26396  el2spthonot  26397  el2wlkonotot0  26399  qqhval2  29354  bnj996  30279  dvhopellsm  35424