Theorem 19.42vv 1967

Description: Version of 19.42 2261 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 1964	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.42v 1963	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))
3	1, 2	bitri 277	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1789

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790

This theorem is referenced by:  exdistr2  1968  3exdistr  1970  cgsex4g  3490  ceqsex3v  3496  ceqsex4v  3497  ceqsex8v  3499  elvvv  5712  xpdifid  6139  dfoprab2  7439  resoprab  7499  elrnmpores  7519  ov3  7544  ov6g  7545  oprabex3  7943  xpassen  9028  entrfil  9138  domtrfil  9145  sbthfilem  9151  axaddf  11089  axmulf  11090  catcone0  17691  qqhval2  34223  bnj996  35198  fineqvac  35357  inxpxrn  38855  dmqsblocks  39404  dvhopellsm  41679