Theorem 2exbidv 1902

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

Syntax hints:   → wi 4   ↔ wb 207  ∃wex 1761

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888

This theorem depends on definitions:  df-bi 208  df-ex 1762

This theorem is referenced by:  3exbidv  1903  4exbidv  1904  cbvex4v  2393  ceqsex3v  3488  ceqsex4v  3489  2reu5  3683  copsexg  5273  euotd  5294  elopab  5304  elxpi  5465  relop  5607  dfres3  5739  xpdifid  5901  oprabv  7073  cbvoprab3  7101  elrnmpores  7144  ov6g  7168  omxpenlem  8465  dcomex  9715  ltresr  10408  hashle2prv  13682  fsumcom2  14962  fprodcom2  15171  ispos  17386  fsumvma  25471  1pthon2v  27619  dfconngr1  27654  isconngr  27655  isconngr1  27656  1conngr  27660  conngrv2edg  27661  fusgr2wsp2nb  27805  isacycgr  32000  satfv1  32218  sat1el2xp  32234  elfuns  32985  bj-cbvex4vv  33674  itg2addnclem3  34476  brxrn2  35158  dvhopellsm  37784  diblsmopel  37838  2sbc5g  40286  ichexmpl1  43113  ichnreuop  43116  ichreuopeq  43117  elsprel  43119  prprelb  43160  reuopreuprim  43170