Theorem 19.41vv 1982

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  19.41vvv  1983  cgsex4g  3496  rabxp  5698  copsex2gb  5783  mpomptx  7534  xpassen  9094  dfac5lem1  10206  fusgr2wsp2nb  30941  bnj996  35633  dfdm5  36630  dfrn5  36631  elima4  36633  brtxp2  36736  brpprod3a  36741  brimg  36792  lemsuccf  36796  brxrn2  39410  diblsmopel  42322  en2pr  44642  mpomptx2  49541