Theorem 2exbidv 1931

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

Syntax hints:   → wi 4   ↔ wb 207  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  3exbidv  1932  4exbidv  1933  cbvex4vw  2049  cbvex4v  2423  ceqsex3v  3486  ceqsex4v  3487  2reu5  3706  opabbidv  5145  unopab  5159  copsexgw  5437  copsexgwOLD  5438  copsexg  5439  euotd  5461  elopabw  5475  elxpi  5647  relop  5799  dfres3  5943  xpdifid  6126  oprabv  7423  cbvoprab3  7454  elrnmpores  7501  ov6g  7527  omxpenlem  9013  dcomex  10367  ltresr  11061  hashle2prv  14438  fsumcom2  15734  fprodcom2  15947  ispos  18278  fsumvma  27201  1pthon2v  30248  dfconngr1  30283  isconngr  30284  isconngr1  30285  1conngr  30289  conngrv2edg  30290  fusgr2wsp2nb  30429  isacycgr  35380  satfv1  35598  sat1el2xp  35614  elfuns  36148  cbvoprab1vw  36472  cbvoprab1davw  36506  cbvoprab3davw  36508  bj-cbvex4vv  37165  itg2addnclem3  38047  brxrn2  38758  dvhopellsm  41616  diblsmopel  41670  2sbc5g  44867  fundcmpsurinj  47891  ichexmpl1  47951  ichnreuop  47954  ichreuopeq  47955  elsprel  47957  prprelb  47998  reuopreuprim  48008  nelsubc3lem  49567  cnelsubclem  50100