Theorem 2exbidv 1926

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 1923	. 2 ⊢ (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
3	2	exbidv 1923	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  3exbidv  1927  4exbidv  1928  cbvex4vw  2044  cbvex4v  2420  ceqsex3v  3484  ceqsex4v  3485  2reu5  3705  opabbidv  5152  unopab  5166  copsexgw  5438  copsexg  5439  euotd  5461  elopabw  5474  elxpi  5646  relop  5799  dfres3  5943  xpdifid  6126  oprabv  7420  cbvoprab3  7451  elrnmpores  7498  ov6g  7524  omxpenlem  9009  dcomex  10360  ltresr  11054  hashle2prv  14431  fsumcom2  15727  fprodcom2  15940  ispos  18271  fsumvma  27190  1pthon2v  30238  dfconngr1  30273  isconngr  30274  isconngr1  30275  1conngr  30279  conngrv2edg  30280  fusgr2wsp2nb  30419  isacycgr  35343  satfv1  35561  sat1el2xp  35577  elfuns  36111  cbvoprab1vw  36435  cbvoprab1davw  36469  cbvoprab3davw  36471  bj-cbvex4vv  37128  itg2addnclem3  38008  brxrn2  38719  dvhopellsm  41577  diblsmopel  41631  2sbc5g  44861  fundcmpsurinj  47881  ichexmpl1  47941  ichnreuop  47944  ichreuopeq  47945  elsprel  47947  prprelb  47988  reuopreuprim  47998  nelsubc3lem  49557  cnelsubclem  50090