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 206  ∃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 207  df-ex 1781

This theorem is referenced by:  3exbidv  1926  4exbidv  1927  cbvex4vw  2043  cbvex4v  2419  ceqsex3v  3495  ceqsex4v  3496  2reu5  3716  opabbidv  5164  unopab  5178  copsexgw  5438  copsexg  5439  euotd  5461  elopabw  5474  elxpi  5646  relop  5799  dfres3  5943  xpdifid  6126  oprabv  7418  cbvoprab3  7449  elrnmpores  7496  ov6g  7522  omxpenlem  9006  dcomex  10357  ltresr  11051  hashle2prv  14401  fsumcom2  15697  fprodcom2  15907  ispos  18237  fsumvma  27180  1pthon2v  30228  dfconngr1  30263  isconngr  30264  isconngr1  30265  1conngr  30269  conngrv2edg  30270  fusgr2wsp2nb  30409  isacycgr  35339  satfv1  35557  sat1el2xp  35573  elfuns  36107  cbvoprab1vw  36431  cbvoprab1davw  36465  cbvoprab3davw  36467  bj-cbvex4vv  37006  itg2addnclem3  37870  brxrn2  38565  dvhopellsm  41373  diblsmopel  41427  2sbc5g  44653  fundcmpsurinj  47651  ichexmpl1  47711  ichnreuop  47714  ichreuopeq  47715  elsprel  47717  prprelb  47758  reuopreuprim  47768  nelsubc3lem  49311  cnelsubclem  49844