Theorem 2exbidv 1928

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

Syntax hints:   → wi 4   ↔ wb 205  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  3exbidv  1929  4exbidv  1930  cbvex4vw  2046  cbvex4v  2415  ceqsex3v  3474  ceqsex4v  3475  2reu5  3688  opabbidv  5136  unopab  5152  copsexgw  5398  copsexg  5399  euotd  5421  elopab  5433  elxpi  5602  relop  5748  dfres3  5885  xpdifid  6060  oprabv  7313  cbvoprab3  7344  elrnmpores  7389  ov6g  7414  omxpenlem  8813  dcomex  10134  ltresr  10827  hashle2prv  14120  fsumcom2  15414  fprodcom2  15622  ispos  17947  fsumvma  26266  1pthon2v  28418  dfconngr1  28453  isconngr  28454  isconngr1  28455  1conngr  28459  conngrv2edg  28460  fusgr2wsp2nb  28599  isacycgr  33007  satfv1  33225  sat1el2xp  33241  elfuns  34144  bj-cbvex4vv  34914  itg2addnclem3  35757  brxrn2  36432  dvhopellsm  39058  diblsmopel  39112  2sbc5g  41923  fundcmpsurinj  44749  ichexmpl1  44809  ichnreuop  44812  ichreuopeq  44813  elsprel  44815  prprelb  44856  reuopreuprim  44866