Theorem 19.42vv 1955

Description: Version of 19.42 2234 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 1952	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.42v 1951	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))
3	1, 2	bitri 275	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1776

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777

This theorem is referenced by:  exdistr2  1956  3exdistr  1958  cgsex4g  3526  ceqsex3v  3537  ceqsex4v  3538  ceqsex8v  3540  elvvv  5764  xpdifid  6190  dfoprab2  7491  resoprab  7551  elrnmpores  7571  ov3  7596  ov6g  7597  oprabex3  8001  xpassen  9105  entrfil  9223  domtrfil  9230  sbthfilem  9236  axaddf  11183  axmulf  11184  catcone0  17732  qqhval2  33945  bnj996  34949  fineqvac  35090  inxpxrn  38377  dvhopellsm  41100