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  2041  cbvex4v  2420  ceqsex3v  3537  ceqsex4v  3538  2reu5  3764  opabbidv  5209  unopab  5224  copsexgw  5495  copsexg  5496  euotd  5518  elopabw  5531  elxpi  5707  relop  5861  dfres3  6002  xpdifid  6188  oprabv  7493  cbvoprab3  7524  elrnmpores  7571  ov6g  7597  omxpenlem  9113  dcomex  10487  ltresr  11180  hashle2prv  14517  fsumcom2  15810  fprodcom2  16020  ispos  18360  fsumvma  27257  1pthon2v  30172  dfconngr1  30207  isconngr  30208  isconngr1  30209  1conngr  30213  conngrv2edg  30214  fusgr2wsp2nb  30353  isacycgr  35150  satfv1  35368  sat1el2xp  35384  elfuns  35916  cbvoprab1vw  36238  cbvoprab1davw  36272  cbvoprab3davw  36274  bj-cbvex4vv  36806  itg2addnclem3  37680  brxrn2  38376  dvhopellsm  41119  diblsmopel  41173  2sbc5g  44435  fundcmpsurinj  47396  ichexmpl1  47456  ichnreuop  47459  ichreuopeq  47460  elsprel  47462  prprelb  47503  reuopreuprim  47513