Theorem 19.42vv 1957

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  exdistr2  1958  3exdistr  1960  cgsex4g  3507  ceqsex3v  3516  ceqsex4v  3517  ceqsex8v  3519  elvvv  5730  xpdifid  6157  dfoprab2  7465  resoprab  7525  elrnmpores  7545  ov3  7570  ov6g  7571  oprabex3  7976  xpassen  9080  entrfil  9199  domtrfil  9206  sbthfilem  9212  axaddf  11159  axmulf  11160  catcone0  17699  qqhval2  34013  bnj996  34987  fineqvac  35128  inxpxrn  38413  dvhopellsm  41136