Theorem 19.42vv 1953

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

Syntax hints:   ↔ wb 205   ∧ wa 394  ∃wex 1773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774

This theorem is referenced by:  exdistr2  1954  3exdistr  1956  cgsex4g  3509  ceqsex3v  3521  ceqsex4v  3522  ceqsex8v  3524  elvvv  5753  xpdifid  6174  dfoprab2  7478  resoprab  7538  elrnmpores  7559  ov3  7584  ov6g  7585  oprabex3  7982  xpassen  9094  entrfil  9216  domtrfil  9223  sbthfilem  9229  axaddf  11175  axmulf  11176  catcone0  17686  qqhval2  33734  bnj996  34738  fineqvac  34868  inxpxrn  38017  dvhopellsm  40740