Theorem 19.42vv 1958

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781

This theorem is referenced by:  exdistr2  1959  3exdistr  1961  cgsex4g  3483  ceqsex3v  3491  ceqsex4v  3492  ceqsex8v  3494  elvvv  5687  xpdifid  6110  dfoprab2  7399  resoprab  7459  elrnmpores  7479  ov3  7504  ov6g  7505  oprabex3  7904  xpassen  8979  entrfil  9089  domtrfil  9096  sbthfilem  9102  axaddf  11031  axmulf  11032  catcone0  17588  qqhval2  33987  bnj996  34960  fineqvac  35131  inxpxrn  38427  dmqsblocks  38891  dvhopellsm  41156