Theorem 19.41vv 1948

Description: Version of 19.41 2233 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 1947	. . 3 ⊢ (∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑦𝜑 ∧ 𝜓))
2	1	exbii 1845	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(∃𝑦𝜑 ∧ 𝜓))
3		19.41v 1947	. 2 ⊢ (∃𝑥(∃𝑦𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓))
4	2, 3	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:  19.41vvv  1949  cgsex4g  3526  rabxp  5737  copsex2gb  5819  mpomptx  7546  xpassen  9105  dfac5lem1  10161  fusgr2wsp2nb  30363  bnj996  34949  dfdm5  35754  dfrn5  35755  elima4  35757  brtxp2  35863  brpprod3a  35868  brimg  35919  brsuccf  35923  brxrn2  38357  diblsmopel  41154  en2pr  43537  mpomptx2  48180