Theorem 2exbidv 1925

Description: Formula-building rule for two existential quantifiers (deduction form). (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 1922	. 2 ⊢ (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
3	2	exbidv 1922	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒))

Syntax hints:   → wi 4   ↔ wb 208  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-ex 1781

This theorem is referenced by:  3exbidv  1926  4exbidv  1927  cbvex4vw  2049  cbvex4v  2437  ceqsex3v  3545  ceqsex4v  3546  2reu5  3749  copsexgw  5381  copsexg  5382  euotd  5403  elopab  5414  elxpi  5577  relop  5721  dfres3  5858  xpdifid  6025  oprabv  7214  cbvoprab3  7245  elrnmpores  7288  ov6g  7312  omxpenlem  8618  dcomex  9869  ltresr  10562  hashle2prv  13837  fsumcom2  15129  fprodcom2  15338  ispos  17557  fsumvma  25789  1pthon2v  27932  dfconngr1  27967  isconngr  27968  isconngr1  27969  1conngr  27973  conngrv2edg  27974  fusgr2wsp2nb  28113  isacycgr  32392  satfv1  32610  sat1el2xp  32626  elfuns  33376  bj-cbvex4vv  34127  itg2addnclem3  34960  brxrn2  35642  dvhopellsm  38268  diblsmopel  38322  2sbc5g  40768  fundcmpsurinj  43589  ichexmpl1  43651  ichnreuop  43654  ichreuopeq  43655  elsprel  43657  prprelb  43698  reuopreuprim  43708