Theorem 19.41vv 1902

Description: Version of 19.41 2090 with two quantifiers and a dv 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 1901	. . 3 ⊢ (∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑦𝜑 ∧ 𝜓))
2	1	exbii 1764	. 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(∃𝑦𝜑 ∧ 𝜓))
3		19.41v 1901	. 2 ⊢ (∃𝑥(∃𝑦𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓))
4	2, 3	bitri 263	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓))

Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696

This theorem is referenced by:  19.41vvv  1903  rabxp  5078  copsex2gb  5153  mpt2mptx  6649  xpassen  7939  dfac5lem1  8829  3v3e3cycl  26193  bnj996  30279  dfdm5  30921  dfrn5  30922  elima4  30924  brtxp2  31158  brpprod3a  31163  brimg  31214  brsuccf  31218  diblsmopel  35478  fusgr2wsp2nb  41498  mpt2mptx2  41906