Theorem 2exbidv 1954

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

Syntax hints:   → wi 4   ↔ wb 209  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

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

This theorem is referenced by:  3exbidv  1955  4exbidv  1956  cbvex4vw  2072  cbvex4v  2447  ceqsex3v  3507  ceqsex4v  3508  2reu5  3722  opabbidv  5178  unopab  5192  copsexgw  5474  copsexgwOLD  5475  copsexg  5476  euotd  5498  elopabw  5512  elxpi  5685  relop  5838  dfres3  5985  xpdifid  6167  xpdifcnvepel  6168  oprabv  7472  cbvoprab3  7503  elrnmpores  7550  ov6g  7576  omxpenlem  9067  dcomex  10432  ltresr  11126  hashle2prv  14517  fsumcom2  15827  fprodcom2  16040  ispos  18371  fsumvma  27355  1pthon2v  30482  dfconngr1  30517  isconngr  30518  isconngr1  30519  1conngr  30523  conngrv2edg  30524  fusgr2wsp2nb  30663  isacycgr  35615  satfv1  35833  sat1el2xp  35849  elfuns  36383  cbvoprab1vw  36727  cbvoprab1davw  36761  cbvoprab3davw  36763  bj-cbvex4vv  37418  itg2addnclem3  38302  brxrn2  39011  dvhopellsm  41869  diblsmopel  41923  2sbc5g  45106  fundcmpsurinj  48135  ichexmpl1  48195  ichnreuop  48198  ichreuopeq  48199  elsprel  48201  prprelb  48242  reuopreuprim  48252  nelsubc3lem  49825  cnelsubclem  50358