Theorem 19.42vv 1959

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  exdistr2  1960  3exdistr  1962  cgsex4g  3489  ceqsex3v  3497  ceqsex4v  3498  ceqsex8v  3500  elvvv  5708  xpdifid  6134  dfoprab2  7426  resoprab  7486  elrnmpores  7506  ov3  7531  ov6g  7532  oprabex3  7931  xpassen  9011  entrfil  9121  domtrfil  9128  sbthfilem  9134  axaddf  11068  axmulf  11069  catcone0  17622  qqhval2  34160  bnj996  35132  fineqvac  35294  inxpxrn  38669  dmqsblocks  39218  dvhopellsm  41493