Theorem 19.42vv 1958

Description: Version of 19.42 2236 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 1955	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.42v 1954	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))
3	1, 2	bitri 278	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 399  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782

This theorem is referenced by:  exdistr2  1959  19.42vvvOLD  1961  3exdistr  1962  ceqsex3v  3493  ceqsex4v  3494  ceqsex8v  3496  elvvv  5591  xpdifid  5992  dfoprab2  7191  resoprab  7249  elrnmpores  7267  ov3  7291  ov6g  7292  oprabex3  7660  xpassen  8594  axaddf  10556  axmulf  10557  qqhval2  31333  bnj996  32338  inxpxrn  35803  dvhopellsm  38413