Theorem 2exbidv 1852

Description: Formula-building rule for two existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.)

Hypothesis

Ref	Expression
2albidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
2exbidv	⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)

Proof of Theorem 2exbidv

Step	Hyp	Ref	Expression
1		2albidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	exbidv 1850	. 2 ⊢ (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
3	2	exbidv 1850	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒))

Syntax hints:   → wi 4   ↔ wb 196  ∃wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  3exbidv  1853  4exbidv  1854  cbvex4v  2289  ceqsex3v  3246  ceqsex4v  3247  2reu5  3416  copsexg  4956  euotd  4975  elopab  4983  elxpi  5130  relop  5272  dfres3  5403  xpdifid  5562  oprabv  6703  cbvoprab3  6731  elrnmpt2res  6774  ov6g  6798  omxpenlem  8061  dcomex  9269  ltresr  9961  hashle2prv  13260  fsumcom2  14505  fsumcom2OLD  14506  fprodcom2  14714  fprodcom2OLD  14715  ispos  16947  fsumvma  24938  1pthon2v  27013  dfconngr1  27048  isconngr  27049  isconngr1  27050  1conngr  27054  conngrv2edg  27055  fusgr2wsp2nb  27198  elfuns  32022  bj-cbvex4vv  32743  itg2addnclem3  33463  dvhopellsm  36406  diblsmopel  36460  2sbc5g  38617  elsprel  41725