Theorem 2exbidv 1928

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

Syntax hints:   → wi 4   ↔ wb 205  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

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

This theorem is referenced by:  3exbidv  1929  4exbidv  1930  cbvex4vw  2046  cbvex4v  2415  ceqsex3v  3532  ceqsex4v  3533  2reu5  3754  opabbidv  5214  unopab  5230  copsexgw  5490  copsexg  5491  euotd  5513  elopabw  5526  elxpi  5698  relop  5849  dfres3  5985  xpdifid  6165  oprabv  7466  cbvoprab3  7497  elrnmpores  7543  ov6g  7568  omxpenlem  9070  dcomex  10439  ltresr  11132  hashle2prv  14436  fsumcom2  15717  fprodcom2  15925  ispos  18264  fsumvma  26706  1pthon2v  29396  dfconngr1  29431  isconngr  29432  isconngr1  29433  1conngr  29437  conngrv2edg  29438  fusgr2wsp2nb  29577  isacycgr  34125  satfv1  34343  sat1el2xp  34359  elfuns  34876  bj-cbvex4vv  35672  itg2addnclem3  36530  brxrn2  37234  dvhopellsm  39977  diblsmopel  40031  2sbc5g  43161  fundcmpsurinj  46064  ichexmpl1  46124  ichnreuop  46127  ichreuopeq  46128  elsprel  46130  prprelb  46171  reuopreuprim  46181