Theorem 19.42vv 2056

Description: Version of 19.42 2280 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 2053	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.42v 2052	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))
3	1, 2	bitri 267	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))

Syntax hints:   ↔ wb 198   ∧ wa 386  ∃wex 1878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879

This theorem is referenced by:  19.42vvv  2057  exdistr2  2058  3exdistr  2059  ceqsex3v  3463  ceqsex4v  3464  ceqsex8v  3466  elvvv  5415  xpdifid  5807  dfoprab2  6966  resoprab  7021  elrnmpt2res  7039  ov3  7062  ov6g  7063  oprabex3  7422  xpassen  8329  axaddf  10289  axmulf  10290  qqhval2  30567  bnj996  31567  cnfinltrel  33781  inxpxrn  34696  dvhopellsm  37187