Theorem 19.42vv 1960

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

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃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 1912

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781

This theorem is referenced by:  exdistr2  1961  3exdistr  1963  ceqsex3v  3493  ceqsex4v  3494  ceqsex8v  3496  elvvv  5687  xpdifid  6100  dfoprab2  7387  resoprab  7446  elrnmpores  7465  ov3  7489  ov6g  7490  oprabex3  7880  xpassen  8923  entrfil  9045  domtrfil  9052  sbthfilem  9058  axaddf  10994  axmulf  10995  catcone0  17485  qqhval2  32171  bnj996  33176  fineqvac  33306  inxpxrn  36655  dvhopellsm  39378