Theorem 2exbidv 1925

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  3exbidv  1926  4exbidv  1927  cbvex4vw  2043  cbvex4v  2417  ceqsex3v  3492  ceqsex4v  3493  2reu5  3713  opabbidv  5159  unopab  5173  copsexgw  5433  copsexg  5434  euotd  5456  elopabw  5469  elxpi  5641  relop  5794  dfres3  5937  xpdifid  6120  oprabv  7412  cbvoprab3  7443  elrnmpores  7490  ov6g  7516  omxpenlem  8998  dcomex  10345  ltresr  11038  hashle2prv  14387  fsumcom2  15683  fprodcom2  15893  ispos  18222  fsumvma  27152  1pthon2v  30135  dfconngr1  30170  isconngr  30171  isconngr1  30172  1conngr  30176  conngrv2edg  30177  fusgr2wsp2nb  30316  isacycgr  35210  satfv1  35428  sat1el2xp  35444  elfuns  35978  cbvoprab1vw  36302  cbvoprab1davw  36336  cbvoprab3davw  36338  bj-cbvex4vv  36870  itg2addnclem3  37734  brxrn2  38429  dvhopellsm  41237  diblsmopel  41291  2sbc5g  44534  fundcmpsurinj  47534  ichexmpl1  47594  ichnreuop  47597  ichreuopeq  47598  elsprel  47600  prprelb  47641  reuopreuprim  47651  nelsubc3lem  49196  cnelsubclem  49729