Theorem 19.41vv 1958

Description: Version of 19.41 2232 with two quantifiers and a disjoint variable condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.)

Assertion

Ref	Expression
19.41vv	⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓))

Distinct variable groups:   𝜓,𝑥   𝜓,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem 19.41vv

Step	Hyp	Ref	Expression
1		19.41v 1957	. . 3 ⊢ (∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑦𝜑 ∧ 𝜓))
2	1	exbii 1854	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(∃𝑦𝜑 ∧ 𝜓))
3		19.41v 1957	. 2 ⊢ (∃𝑥(∃𝑦𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓))
4	2, 3	bitri 274	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787

This theorem is referenced by:  19.41vvv  1959  rabxp  5636  copsex2gb  5715  mpomptx  7382  xpassen  8844  dfac5lem1  9890  fusgr2wsp2nb  28707  bnj996  32945  dfdm5  33756  dfrn5  33757  elima4  33759  brtxp2  34192  brpprod3a  34197  brimg  34248  brsuccf  34252  brxrn2  36514  diblsmopel  39194  en2pr  41136  mpomptx2  45649