Theorem 2exbidv 1923

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  3exbidv  1924  4exbidv  1925  cbvex4vw  2041  cbvex4v  2423  ceqsex3v  3549  ceqsex4v  3550  2reu5  3780  opabbidv  5232  unopab  5248  copsexgw  5510  copsexg  5511  euotd  5532  elopabw  5545  elxpi  5722  relop  5875  dfres3  6014  xpdifid  6199  oprabv  7510  cbvoprab3  7541  elrnmpores  7588  ov6g  7614  omxpenlem  9139  dcomex  10516  ltresr  11209  hashle2prv  14527  fsumcom2  15822  fprodcom2  16032  ispos  18384  fsumvma  27275  1pthon2v  30185  dfconngr1  30220  isconngr  30221  isconngr1  30222  1conngr  30226  conngrv2edg  30227  fusgr2wsp2nb  30366  isacycgr  35113  satfv1  35331  sat1el2xp  35347  elfuns  35879  cbvoprab1vw  36203  cbvoprab1davw  36237  cbvoprab3davw  36239  bj-cbvex4vv  36771  itg2addnclem3  37633  brxrn2  38331  dvhopellsm  41074  diblsmopel  41128  2sbc5g  44385  fundcmpsurinj  47283  ichexmpl1  47343  ichnreuop  47346  ichreuopeq  47347  elsprel  47349  prprelb  47390  reuopreuprim  47400