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

Theorem 2exbidv 1997
 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 1995 . 2 (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
32exbidv 1995 1 (𝜑 → (∃𝑥𝑦𝜓 ↔ ∃𝑥𝑦𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196  ∃wex 1849 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984 This theorem depends on definitions:  df-bi 197  df-ex 1850 This theorem is referenced by:  3exbidv  1998  4exbidv  1999  cbvex4v  2430  ceqsex3v  3382  ceqsex4v  3383  2reu5  3553  copsexg  5100  euotd  5119  elopab  5129  elxpi  5283  relop  5424  dfres3  5552  xpdifid  5716  oprabv  6864  cbvoprab3  6892  elrnmpt2res  6935  ov6g  6959  omxpenlem  8222  dcomex  9457  ltresr  10149  hashle2prv  13448  fsumcom2  14700  fsumcom2OLD  14701  fprodcom2  14909  fprodcom2OLD  14910  ispos  17144  fsumvma  25133  1pthon2v  27301  dfconngr1  27336  isconngr  27337  isconngr1  27338  1conngr  27342  conngrv2edg  27343  fusgr2wsp2nb  27484  elfuns  32324  bj-cbvex4vv  33045  itg2addnclem3  33772  brxrn2  34456  dvhopellsm  36904  diblsmopel  36958  2sbc5g  39115  elsprel  42231
 Copyright terms: Public domain W3C validator