Theorem 2exbidv 1957

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

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

This theorem is used by:  3exbidv  1958  4exbidv  1959  cbvex4vw  2075  cbvex4v  2450  ceqsex3v  3510  ceqsex4v  3511  2reu5  3724  opabbidv  5182  unopab  5196  copsexgw  5477  copsexgwOLD  5478  copsexg  5479  euotd  5501  elopabw  5515  elxpi  5688  relop  5841  dfres3  5988  xpdifid  6170  xpdifcnvepel  6171  oprabv  7483  cbvoprab3  7514  elrnmpores  7561  ov6g  7587  omxpenlem  9076  dcomex  10449  ltresr  11143  hashle2prv  14535  fsumcom2  15851  fprodcom2  16064  ispos  18395  fsumvma  27414  1pthon2v  30541  dfconngr1  30576  isconngr  30577  isconngr1  30578  1conngr  30582  conngrv2edg  30583  fusgr2wsp2nb  30722  isacycgr  35658  satfv1  35876  sat1el2xp  35892  elfuns  36426  cbvoprab1vw  36790  cbvoprab1davw  36824  cbvoprab3davw  36826  bj-cbvex4vv  37481  itg2addnclem3  38365  brxrn2  39074  dvhopellsm  41932  diblsmopel  41986  2sbc5g  45167  fundcmpsurinj  48199  ichexmpl1  48259  ichnreuop  48262  ichreuopeq  48263  elsprel  48265  prprelb  48306  reuopreuprim  48316  nelsubc3lem  49889  cnelsubclem  50422