Theorem 19.42vv 1990

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 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  3496  ceqsex3v  3502  ceqsex4v  3503  ceqsex8v  3505  elvvv  5731  xpdifid  6160  xpdifcnvepel  6161  dfoprab2  7471  resoprab  7531  elrnmpores  7551  ov3  7576  ov6g  7577  oprabex3  7974  xpassen  9069  entrfil  9179  domtrfil  9186  sbthfilem  9192  axaddf  11154  axmulf  11155  catcone0  17775  qqhval2  34492  bnj996  35465  fineqvac  35642  inxpxrn  39166  dmqsblocks  39715  dvhopellsm  41990