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

Theorem 2exbidv 1839
 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 1837 . 2 (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
32exbidv 1837 1 (𝜑 → (∃𝑥𝑦𝜓 ↔ ∃𝑥𝑦𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  ∃wex 1695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827 This theorem depends on definitions:  df-bi 196  df-ex 1696 This theorem is referenced by:  3exbidv  1840  4exbidv  1841  cbvex4v  2277  ceqsex3v  3219  ceqsex4v  3220  2reu5  3383  copsexg  4882  euotd  4900  elopab  4908  elxpi  5054  relop  5194  xpdifid  5481  oprabv  6601  cbvoprab3  6629  elrnmpt2res  6672  ov6g  6696  omxpenlem  7946  dcomex  9152  ltresr  9840  fsumcom2  14347  fsumcom2OLD  14348  fprodcom2  14553  fprodcom2OLD  14554  ispos  16770  fsumvma  24738  dfconngra1  26199  isconngra  26200  isconngra1  26201  1conngra  26203  is2wlkonot  26390  is2spthonot  26391  2wlkonot  26392  2spthonot  26393  el2wlkonot  26396  el2spthonot  26397  el2spthonot0  26398  el2wlkonotot0  26399  2wlkonot3v  26402  2spthonot3v  26403  usg2wotspth  26411  2pthwlkonot  26412  2spotdisj  26588  usg2spot2nb  26592  dfres3  30902  elfuns  31192  bj-cbvex4vv  31930  itg2addnclem3  32633  dvhopellsm  35424  diblsmopel  35478  2sbc5g  37639  1pthon2v-av  41320  dfconngr1  41355  isconngr  41356  isconngr1  41357  1conngr  41361  conngrv2edg  41362  fusgr2wsp2nb  41498
 Copyright terms: Public domain W3C validator