Theorem 19.42vv 1990

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

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

This theorem is used by:  exdistr2  1991  3exdistr  1993  cgsex4g  3497  ceqsex3v  3503  ceqsex4v  3504  ceqsex8v  3506  elvvv  5727  xpdifid  6159  xpdifcnvepel  6160  dfoprab2  7476  resoprab  7536  elrnmpores  7556  ov3  7581  ov6g  7582  oprabex3  7987  xpassen  9083  entrfil  9193  domtrfil  9200  sbthfilem  9206  axaddf  11223  axmulf  11224  catcone0  17854  qqhval2  34607  bnj996  35579  fineqvac  35767  coi1in  37941  inxpxrn  39330  dmqsblocks  39879  dvhopellsm  42154