Theorem 19.42vv 1959

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃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 1912

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

This theorem is referenced by:  exdistr2  1960  3exdistr  1962  cgsex4g  3476  ceqsex3v  3483  ceqsex4v  3484  ceqsex8v  3486  elvvv  5707  xpdifid  6132  dfoprab2  7425  resoprab  7485  elrnmpores  7505  ov3  7530  ov6g  7531  oprabex3  7930  xpassen  9009  entrfil  9119  domtrfil  9126  sbthfilem  9132  axaddf  11068  axmulf  11069  catcone0  17653  qqhval2  34126  bnj996  35098  fineqvac  35260  inxpxrn  38739  dmqsblocks  39288  dvhopellsm  41563