Theorem 19.42vv 1992

Description: Version of 19.42 2276 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 1989	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.42v 1988	. 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 1945

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

This theorem is used by:  exdistr2  1993  3exdistr  1995  cgsex4g  3500  ceqsex3v  3506  ceqsex4v  3507  ceqsex8v  3509  elvvv  5735  xpdifid  6177  xpdifcnvepel  6178  dfoprab2  7509  resoprab  7569  elrnmpores  7590  ov3  7615  ov6g  7616  oprabex3  8023  xpassen  9128  entrfil  9238  domtrfil  9245  sbthfilem  9251  axaddf  11269  axmulf  11270  catcone0  17911  qqhval2  34725  bnj996  35697  fineqvac  35925  inxpxrn  39616  dmqsblocks  40165  dvhopellsm  42440