Theorem 2exbidv 1924

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

Syntax hints:   → wi 4   ↔ wb 206  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  3exbidv  1925  4exbidv  1926  cbvex4vw  2042  cbvex4v  2414  ceqsex3v  3506  ceqsex4v  3507  2reu5  3732  opabbidv  5176  unopab  5190  copsexgw  5453  copsexg  5454  euotd  5476  elopabw  5489  elxpi  5663  relop  5817  dfres3  5958  xpdifid  6144  oprabv  7452  cbvoprab3  7483  elrnmpores  7530  ov6g  7556  omxpenlem  9047  dcomex  10407  ltresr  11100  hashle2prv  14450  fsumcom2  15747  fprodcom2  15957  ispos  18282  fsumvma  27131  1pthon2v  30089  dfconngr1  30124  isconngr  30125  isconngr1  30126  1conngr  30130  conngrv2edg  30131  fusgr2wsp2nb  30270  isacycgr  35139  satfv1  35357  sat1el2xp  35373  elfuns  35910  cbvoprab1vw  36232  cbvoprab1davw  36266  cbvoprab3davw  36268  bj-cbvex4vv  36800  itg2addnclem3  37674  brxrn2  38364  dvhopellsm  41118  diblsmopel  41172  2sbc5g  44412  fundcmpsurinj  47414  ichexmpl1  47474  ichnreuop  47477  ichreuopeq  47478  elsprel  47480  prprelb  47521  reuopreuprim  47531  nelsubc3lem  49063  cnelsubclem  49596