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  3477  ceqsex3v  3484  ceqsex4v  3485  ceqsex8v  3487  elvvv  5700  xpdifid  6126  dfoprab2  7418  resoprab  7478  elrnmpores  7498  ov3  7523  ov6g  7524  oprabex3  7923  xpassen  9002  entrfil  9112  domtrfil  9119  sbthfilem  9125  axaddf  11059  axmulf  11060  catcone0  17644  qqhval2  34142  bnj996  35114  fineqvac  35276  inxpxrn  38753  dmqsblocks  39302  dvhopellsm  41577