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  3485  ceqsex3v  3494  ceqsex4v  3495  ceqsex8v  3497  elvvv  5699  xpdifid  6121  dfoprab2  7411  resoprab  7471  elrnmpores  7491  ov3  7516  ov6g  7517  oprabex3  7919  xpassen  8995  entrfil  9109  domtrfil  9116  sbthfilem  9122  axaddf  11058  axmulf  11059  catcone0  17612  qqhval2  33968  bnj996  34942  fineqvac  35091  inxpxrn  38386  dmqsblocks  38850  dvhopellsm  41116