Theorem 19.42vv 1987

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 1984	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.42v 1983	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))
3	1, 2	bitri 278	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810

This theorem is referenced by:  exdistr2  1988  3exdistr  1990  cgsex4g  3501  ceqsex3v  3507  ceqsex4v  3508  ceqsex8v  3510  elvvv  5737  xpdifid  6165  xpdifcnvepel  6166  dfoprab2  7468  resoprab  7528  elrnmpores  7548  ov3  7573  ov6g  7574  oprabex3  7970  xpassen  9055  entrfil  9165  domtrfil  9172  sbthfilem  9178  axaddf  11125  axmulf  11126  catcone0  17738  qqhval2  34372  bnj996  35344  fineqvac  35529  inxpxrn  39067  dmqsblocks  39616  dvhopellsm  41891