Theorem 19.42vv 1990

Description: Version of 19.42 2275 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  3503  ceqsex3v  3509  ceqsex4v  3510  ceqsex8v  3512  elvvv  5739  xpdifid  6167  xpdifcnvepel  6168  dfoprab2  7477  resoprab  7537  elrnmpores  7557  ov3  7582  ov6g  7583  oprabex3  7980  xpassen  9066  entrfil  9176  domtrfil  9183  sbthfilem  9189  axaddf  11145  axmulf  11146  catcone0  17765  qqhval2  34436  bnj996  35409  fineqvac  35586  inxpxrn  39125  dmqsblocks  39674  dvhopellsm  41949