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 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  exdistr2  1958  3exdistr  1960  cgsex4g  3538  ceqsex3v  3549  ceqsex4v  3550  ceqsex8v  3552  elvvv  5775  xpdifid  6199  dfoprab2  7508  resoprab  7568  elrnmpores  7588  ov3  7613  ov6g  7614  oprabex3  8018  xpassen  9132  entrfil  9251  domtrfil  9258  sbthfilem  9264  axaddf  11214  axmulf  11215  catcone0  17745  qqhval2  33928  bnj996  34932  fineqvac  35073  inxpxrn  38351  dvhopellsm  41074