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  3483  ceqsex3v  3492  ceqsex4v  3493  ceqsex8v  3495  elvvv  5695  xpdifid  6117  dfoprab2  7407  resoprab  7467  elrnmpores  7487  ov3  7512  ov6g  7513  oprabex3  7912  xpassen  8988  entrfil  9099  domtrfil  9106  sbthfilem  9112  axaddf  11039  axmulf  11040  catcone0  17593  qqhval2  33949  bnj996  34923  fineqvac  35072  inxpxrn  38367  dmqsblocks  38831  dvhopellsm  41096