Theorem 19.42vv 1984

Description: Version of 19.42 2278 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 1981	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.42v 1980	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))
3	1, 2	bitri 278	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807

This theorem is referenced by:  exdistr2  1985  3exdistr  1987  cgsex4g  3509  ceqsex3v  3515  ceqsex4v  3516  ceqsex8v  3518  elvvv  5738  xpdifid  6166  xpdifcnvepel  6167  dfoprab2  7469  resoprab  7529  elrnmpores  7549  ov3  7574  ov6g  7575  oprabex3  7973  xpassen  9058  entrfil  9168  domtrfil  9175  sbthfilem  9181  axaddf  11129  axmulf  11130  catcone0  17742  qqhval2  34316  bnj996  35288  fineqvac  35451  inxpxrn  38956  dmqsblocks  39505  dvhopellsm  41780