Theorem 19.42vv 1957

Description: Version of 19.42 2237 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  3494  ceqsex3v  3503  ceqsex4v  3504  ceqsex8v  3506  elvvv  5714  xpdifid  6141  dfoprab2  7447  resoprab  7507  elrnmpores  7527  ov3  7552  ov6g  7553  oprabex3  7956  xpassen  9035  entrfil  9149  domtrfil  9156  sbthfilem  9162  axaddf  11098  axmulf  11099  catcone0  17648  qqhval2  33972  bnj996  34946  fineqvac  35087  inxpxrn  38381  dmqsblocks  38845  dvhopellsm  41111