Theorem 2exbidv 1959

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

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

This theorem is used by:  3exbidv  1960  4exbidv  1961  cbvex4vw  2077  cbvex4v  2447  ceqsex3v  3506  ceqsex4v  3507  2reu5  3719  opabbidv  5174  unopab  5188  copsexgw  5464  copsexgwOLD  5465  copsexg  5466  euotd  5490  elopabw  5504  elxpi  5677  relop  5834  dfres3  5986  xpdifid  6171  xpdifcnvepel  6172  oprabv  7503  cbvoprab3  7534  elrnmpores  7582  ov6g  7608  omxpenlem  9125  dcomex  10552  ltresr  11252  hashle2prv  14650  fsumcom2  15969  fprodcom2  16180  ispos  18517  fsumvma  27570  isacycgr  30781  1pthon2v  30784  dfconngr1  30819  isconngr  30820  isconngr1  30821  1conngr  30825  conngrv2edg  30826  fusgr2wsp2nb  30965  mpofvd  35797  satfv1  36295  sat1el2xp  36311  elfuns  36855  cbvoprab1vw  37204  cbvoprab1davw  37238  cbvoprab3davw  37240  bj-cbvex4vv  37895  itg2addnclem3  38783  brxrn2  39508  dvhopellsm  42366  diblsmopel  42420  2sbc5g  45592  fundcmpsurinj  48696  ichexmpl1  48756  ichnreuop  48759  ichreuopeq  48760  elsprel  48762  prprelb  48803  reuopreuprim  48813  nelsubc3lem  50389  cnelsubcw  50946