Theorem 19.42vv 1977

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

Syntax hints:   ↔ wb 208   ∧ wa 399  ∃wex 1799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800

This theorem is referenced by:  exdistr2  1978  3exdistr  1980  cgsex4g  3500  ceqsex3v  3506  ceqsex4v  3507  ceqsex8v  3509  elvvv  5723  xpdifid  6153  xpdifcnvepel  6154  dfoprab2  7454  resoprab  7514  elrnmpores  7534  ov3  7559  ov6g  7560  oprabex3  7958  xpassen  9043  entrfil  9153  domtrfil  9160  sbthfilem  9166  axaddf  11103  axmulf  11104  catcone0  17719  qqhval2  34276  bnj996  35248  fineqvac  35409  inxpxrn  38914  dmqsblocks  39463  dvhopellsm  41738