Theorem 2exbidv 1993

Description: Formula-building rule for two existential quantifiers (deduction rule). (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 1991	. 2 ⊢ (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
3	2	exbidv 1991	1 ⊢ (𝜑 → (∃𝑥∃𝑦𝜓 ↔ ∃𝑥∃𝑦𝜒))

Syntax hints:   → wi 4   ↔ wb 196  ∃wex 1845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980

This theorem depends on definitions:  df-bi 197  df-ex 1846

This theorem is referenced by:  3exbidv  1994  4exbidv  1995  cbvex4v  2426  ceqsex3v  3378  ceqsex4v  3379  2reu5  3549  copsexg  5096  euotd  5115  elopab  5125  elxpi  5279  relop  5420  dfres3  5548  xpdifid  5712  oprabv  6860  cbvoprab3  6888  elrnmpt2res  6931  ov6g  6955  omxpenlem  8218  dcomex  9453  ltresr  10145  hashle2prv  13444  fsumcom2  14696  fsumcom2OLD  14697  fprodcom2  14905  fprodcom2OLD  14906  ispos  17140  fsumvma  25129  1pthon2v  27297  dfconngr1  27332  isconngr  27333  isconngr1  27334  1conngr  27338  conngrv2edg  27339  fusgr2wsp2nb  27480  elfuns  32320  bj-cbvex4vv  33041  itg2addnclem3  33768  brxrn2  34452  dvhopellsm  36900  diblsmopel  36954  2sbc5g  39111  elsprel  42227