Theorem 19.42vv 1958

Description: Version of 19.42 2243 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  3487  ceqsex3v  3495  ceqsex4v  3496  ceqsex8v  3498  elvvv  5700  xpdifid  6126  dfoprab2  7416  resoprab  7476  elrnmpores  7496  ov3  7521  ov6g  7522  oprabex3  7921  xpassen  8999  entrfil  9109  domtrfil  9116  sbthfilem  9122  axaddf  11056  axmulf  11057  catcone0  17610  qqhval2  34139  bnj996  35112  fineqvac  35272  inxpxrn  38603  dmqsblocks  39112  dvhopellsm  41377