Theorem 19.42vv 1923

Description: Version of 19.42 2143 with two quantifiers and a dv 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 1922	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2		19.42v 1921	. 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))
3	1, 2	bitri 264	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓))

Syntax hints:   ↔ wb 196   ∧ wa 383  ∃wex 1744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745

This theorem is referenced by:  19.42vvv  1924  exdistr2  1925  3exdistr  1926  ceqsex3v  3277  ceqsex4v  3278  ceqsex8v  3280  elvvv  5212  xpdifid  5597  dfoprab2  6743  resoprab  6798  elrnmpt2res  6816  ov3  6839  ov6g  6840  oprabex3  7199  xpassen  8095  axaddf  10004  axmulf  10005  qqhval2  30154  bnj996  31151  inxpxrn  34293  dvhopellsm  36723