Theorem 2exbidv 1926

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

Syntax hints:   → wi 4   ↔ wb 209  ∃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 1912

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

This theorem is referenced by:  3exbidv  1927  4exbidv  1928  cbvex4vw  2050  cbvex4v  2427  ceqsex3v  3463  ceqsex4v  3464  2reu5  3673  opabbidv  5099  copsexgw  5350  copsexg  5351  euotd  5373  elopab  5385  elxpi  5547  relop  5691  dfres3  5829  xpdifid  5998  oprabv  7209  cbvoprab3  7240  elrnmpores  7284  ov6g  7309  omxpenlem  8639  dcomex  9900  ltresr  10593  hashle2prv  13881  fsumcom2  15170  fprodcom2  15379  ispos  17616  fsumvma  25889  1pthon2v  28030  dfconngr1  28065  isconngr  28066  isconngr1  28067  1conngr  28071  conngrv2edg  28072  fusgr2wsp2nb  28211  isacycgr  32616  satfv1  32834  sat1el2xp  32850  elfuns  33759  bj-cbvex4vv  34516  itg2addnclem3  35383  brxrn2  36060  dvhopellsm  38686  diblsmopel  38740  2sbc5g  41486  fundcmpsurinj  44287  ichexmpl1  44347  ichnreuop  44350  ichreuopeq  44351  elsprel  44353  prprelb  44394  reuopreuprim  44404