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  3530  ceqsex4v  3531  2reu5  3752  opabbidv  5210  unopab  5226  copsexgw  5486  copsexg  5487  euotd  5509  elopabw  5522  elxpi  5694  relop  5845  dfres3  5981  xpdifid  6159  oprabv  7456  cbvoprab3  7487  elrnmpores  7533  ov6g  7558  omxpenlem  9061  dcomex  10429  ltresr  11122  hashle2prv  14426  fsumcom2  15707  fprodcom2  15915  ispos  18254  fsumvma  26683  1pthon2v  29373  dfconngr1  29408  isconngr  29409  isconngr1  29410  1conngr  29414  conngrv2edg  29415  fusgr2wsp2nb  29554  isacycgr  34067  satfv1  34285  sat1el2xp  34301  elfuns  34818  bj-cbvex4vv  35588  itg2addnclem3  36446  brxrn2  37151  dvhopellsm  39894  diblsmopel  39948  2sbc5g  43046  fundcmpsurinj  45950  ichexmpl1  46010  ichnreuop  46013  ichreuopeq  46014  elsprel  46016  prprelb  46057  reuopreuprim  46067