Theorem 2exbidv 1956

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  3exbidv  1957  4exbidv  1958  cbvex4vw  2074  cbvex4v  2444  ceqsex3v  3502  ceqsex4v  3503  2reu5  3715  opabbidv  5170  unopab  5184  copsexgw  5459  copsexgwOLD  5460  copsexg  5461  euotd  5485  elopabw  5499  elxpi  5672  relop  5827  dfres3  5974  xpdifid  6158  xpdifcnvepel  6159  oprabv  7480  cbvoprab3  7511  elrnmpores  7558  ov6g  7584  omxpenlem  9100  dcomex  10528  ltresr  11228  hashle2prv  14626  fsumcom2  15945  fprodcom2  16156  ispos  18493  fsumvma  27545  isacycgr  30756  1pthon2v  30759  dfconngr1  30794  isconngr  30795  isconngr1  30796  1conngr  30800  conngrv2edg  30801  fusgr2wsp2nb  30940  satfv1  36214  sat1el2xp  36230  elfuns  36769  cbvoprab1vw  37118  cbvoprab1davw  37152  cbvoprab3davw  37154  bj-cbvex4vv  37809  itg2addnclem3  38684  brxrn2  39409  dvhopellsm  42267  diblsmopel  42321  2sbc5g  45493  fundcmpsurinj  48584  ichexmpl1  48644  ichnreuop  48647  ichreuopeq  48648  elsprel  48650  prprelb  48691  reuopreuprim  48701  nelsubc3lem  50277  cnelsubcw  50834