Theorem 19.42vv 1959

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

Syntax hints:   ↔ wb 205   ∧ wa 394  ∃wex 1779

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780

This theorem is referenced by:  exdistr2  1960  3exdistr  1962  cgsex4g  3519  ceqsex3v  3530  ceqsex4v  3531  ceqsex8v  3533  elvvv  5750  xpdifid  6166  dfoprab2  7469  resoprab  7528  elrnmpores  7548  ov3  7572  ov6g  7573  oprabex3  7966  xpassen  9068  entrfil  9190  domtrfil  9197  sbthfilem  9203  axaddf  11142  axmulf  11143  catcone0  17635  qqhval2  33260  bnj996  34265  fineqvac  34395  inxpxrn  37568  dvhopellsm  40291