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 206  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  3exbidv  1927  4exbidv  1928  cbvex4vw  2044  cbvex4v  2420  ceqsex3v  3497  ceqsex4v  3498  2reu5  3718  opabbidv  5166  unopab  5180  copsexgw  5446  copsexg  5447  euotd  5469  elopabw  5482  elxpi  5654  relop  5807  dfres3  5951  xpdifid  6134  oprabv  7428  cbvoprab3  7459  elrnmpores  7506  ov6g  7532  omxpenlem  9018  dcomex  10369  ltresr  11063  hashle2prv  14413  fsumcom2  15709  fprodcom2  15919  ispos  18249  fsumvma  27192  1pthon2v  30240  dfconngr1  30275  isconngr  30276  isconngr1  30277  1conngr  30281  conngrv2edg  30282  fusgr2wsp2nb  30421  isacycgr  35358  satfv1  35576  sat1el2xp  35592  elfuns  36126  cbvoprab1vw  36450  cbvoprab1davw  36484  cbvoprab3davw  36486  bj-cbvex4vv  37047  itg2addnclem3  37918  brxrn2  38629  dvhopellsm  41487  diblsmopel  41541  2sbc5g  44766  fundcmpsurinj  47763  ichexmpl1  47823  ichnreuop  47826  ichreuopeq  47827  elsprel  47829  prprelb  47870  reuopreuprim  47880  nelsubc3lem  49423  cnelsubclem  49956