MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2exbidv Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 2albidv.1 . . 3 (𝜑 → (𝜓𝜒))
21exbidv 1991 . 2 (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
32exbidv 1991 1 (𝜑 → (∃𝑥𝑦𝜓 ↔ ∃𝑥𝑦𝜒))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator