Theorem 19.41vv 1950

Description: Version of 19.41 2236 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 1949	. . 3 ⊢ (∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑦𝜑 ∧ 𝜓))
2	1	exbii 1846	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(∃𝑦𝜑 ∧ 𝜓))
3		19.41v 1949	. 2 ⊢ (∃𝑥(∃𝑦𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓))
4	2, 3	bitri 275	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  19.41vvv  1951  cgsex4g  3538  rabxp  5748  copsex2gb  5830  mpomptx  7563  xpassen  9132  dfac5lem1  10192  fusgr2wsp2nb  30366  bnj996  34932  dfdm5  35736  dfrn5  35737  elima4  35739  brtxp2  35845  brpprod3a  35850  brimg  35901  brsuccf  35905  brxrn2  38331  diblsmopel  41128  en2pr  43509  mpomptx2  48059