Theorem 19.42vv 1952

Description: Version of 19.42 2231 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 1949	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.42v 1948	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))
3	1, 2	bitri 277	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775

This theorem is referenced by:  exdistr2  1953  19.42vvvOLD  1955  3exdistr  1956  ceqsex3v  3544  ceqsex4v  3545  ceqsex8v  3547  elvvv  5620  xpdifid  6018  dfoprab2  7204  resoprab  7262  elrnmpores  7280  ov3  7303  ov6g  7304  oprabex3  7670  xpassen  8603  axaddf  10559  axmulf  10560  qqhval2  31216  bnj996  32221  inxpxrn  35635  dvhopellsm  38245