Theorem 19.42vv 1989

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  exdistr2  1990  3exdistr  1992  cgsex4g  3496  ceqsex3v  3502  ceqsex4v  3503  ceqsex8v  3505  elvvv  5728  xpdifid  6161  xpdifcnvepel  6162  dfoprab2  7482  resoprab  7542  elrnmpores  7562  ov3  7587  ov6g  7588  oprabex3  7993  xpassen  9097  entrfil  9207  domtrfil  9214  sbthfilem  9220  axaddf  11237  axmulf  11238  catcone0  17870  qqhval2  34664  bnj996  35636  fineqvac  35844  inxpxrn  39459  dmqsblocks  40008  dvhopellsm  42283