Theorem 19.42vv 1958

Description: Version of 19.42 2241 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 1955	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.42v 1954	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))
3	1, 2	bitri 275	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781

This theorem is referenced by:  exdistr2  1959  3exdistr  1961  cgsex4g  3484  ceqsex3v  3492  ceqsex4v  3493  ceqsex8v  3495  elvvv  5697  xpdifid  6123  dfoprab2  7413  resoprab  7473  elrnmpores  7493  ov3  7518  ov6g  7519  oprabex3  7918  xpassen  8995  entrfil  9105  domtrfil  9112  sbthfilem  9118  axaddf  11047  axmulf  11048  catcone0  17601  qqhval2  34067  bnj996  35040  fineqvac  35211  inxpxrn  38515  dmqsblocks  39024  dvhopellsm  41289