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  3484  ceqsex4v  3485  2reu5  3705  opabbidv  5152  unopab  5166  copsexgw  5436  copsexg  5437  euotd  5459  elopabw  5472  elxpi  5644  relop  5797  dfres3  5941  xpdifid  6124  oprabv  7418  cbvoprab3  7449  elrnmpores  7496  ov6g  7522  omxpenlem  9007  dcomex  10358  ltresr  11052  hashle2prv  14429  fsumcom2  15725  fprodcom2  15938  ispos  18269  fsumvma  27195  1pthon2v  30243  dfconngr1  30278  isconngr  30279  isconngr1  30280  1conngr  30284  conngrv2edg  30285  fusgr2wsp2nb  30424  isacycgr  35348  satfv1  35566  sat1el2xp  35582  elfuns  36116  cbvoprab1vw  36440  cbvoprab1davw  36474  cbvoprab3davw  36476  bj-cbvex4vv  37125  itg2addnclem3  38005  brxrn2  38716  dvhopellsm  41574  diblsmopel  41628  2sbc5g  44858  fundcmpsurinj  47866  ichexmpl1  47926  ichnreuop  47929  ichreuopeq  47930  elsprel  47932  prprelb  47973  reuopreuprim  47983  nelsubc3lem  49542  cnelsubclem  50075