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 205  ∃wex 1779

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

This theorem depends on definitions:  df-bi 206  df-ex 1780

This theorem is referenced by:  3exbidv  1926  4exbidv  1927  cbvex4vw  2043  cbvex4v  2412  ceqsex3v  3530  ceqsex4v  3531  2reu5  3753  opabbidv  5213  unopab  5229  copsexgw  5489  copsexg  5490  euotd  5512  elopabw  5525  elxpi  5697  relop  5849  dfres3  5985  xpdifid  6166  oprabv  7471  cbvoprab3  7502  elrnmpores  7548  ov6g  7573  omxpenlem  9075  dcomex  10444  ltresr  11137  hashle2prv  14443  fsumcom2  15724  fprodcom2  15932  ispos  18271  fsumvma  26952  1pthon2v  29673  dfconngr1  29708  isconngr  29709  isconngr1  29710  1conngr  29714  conngrv2edg  29715  fusgr2wsp2nb  29854  isacycgr  34434  satfv1  34652  sat1el2xp  34668  elfuns  35191  bj-cbvex4vv  35986  itg2addnclem3  36844  brxrn2  37548  dvhopellsm  40291  diblsmopel  40345  2sbc5g  43477  fundcmpsurinj  46375  ichexmpl1  46435  ichnreuop  46438  ichreuopeq  46439  elsprel  46441  prprelb  46482  reuopreuprim  46492