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  2415  ceqsex3v  3492  ceqsex4v  3493  2reu5  3717  opabbidv  5157  unopab  5171  copsexgw  5430  copsexg  5431  euotd  5453  elopabw  5466  elxpi  5638  relop  5790  dfres3  5933  xpdifid  6115  oprabv  7406  cbvoprab3  7437  elrnmpores  7484  ov6g  7510  omxpenlem  8991  dcomex  10338  ltresr  11031  hashle2prv  14385  fsumcom2  15681  fprodcom2  15891  ispos  18220  fsumvma  27152  1pthon2v  30131  dfconngr1  30166  isconngr  30167  isconngr1  30168  1conngr  30172  conngrv2edg  30173  fusgr2wsp2nb  30312  isacycgr  35187  satfv1  35405  sat1el2xp  35421  elfuns  35955  cbvoprab1vw  36277  cbvoprab1davw  36311  cbvoprab3davw  36313  bj-cbvex4vv  36845  itg2addnclem3  37719  brxrn2  38409  dvhopellsm  41162  diblsmopel  41216  2sbc5g  44455  fundcmpsurinj  47446  ichexmpl1  47506  ichnreuop  47509  ichreuopeq  47510  elsprel  47512  prprelb  47553  reuopreuprim  47563  nelsubc3lem  49108  cnelsubclem  49641