Theorem 2exbidv 1957

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  3exbidv  1958  4exbidv  1959  cbvex4vw  2075  cbvex4v  2445  ceqsex3v  3503  ceqsex4v  3504  2reu5  3716  opabbidv  5171  unopab  5185  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  euotd  5486  elopabw  5500  elxpi  5673  relop  5828  dfres3  5975  xpdifid  6158  xpdifcnvepel  6159  oprabv  7472  cbvoprab3  7503  elrnmpores  7550  ov6g  7576  omxpenlem  9081  dcomex  10506  ltresr  11206  hashle2prv  14603  fsumcom2  15920  fprodcom2  16131  ispos  18468  fsumvma  27522  isacycgr  30733  1pthon2v  30736  dfconngr1  30771  isconngr  30772  isconngr1  30773  1conngr  30777  conngrv2edg  30778  fusgr2wsp2nb  30917  satfv1  36097  sat1el2xp  36113  elfuns  36647  cbvoprab1vw  36996  cbvoprab1davw  37030  cbvoprab3davw  37032  bj-cbvex4vv  37687  itg2addnclem3  38559  brxrn2  39284  dvhopellsm  42142  diblsmopel  42196  2sbc5g  45359  fundcmpsurinj  48435  ichexmpl1  48495  ichnreuop  48498  ichreuopeq  48499  elsprel  48501  prprelb  48542  reuopreuprim  48552  nelsubc3lem  50122  cnelsubclem  50655