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

Theorem 2exbidv 1926
 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
StepHypRef Expression
1 2albidv.1 . . 3 (𝜑 → (𝜓𝜒))
21exbidv 1923 . 2 (𝜑 → (∃𝑦𝜓 ↔ ∃𝑦𝜒))
32exbidv 1923 1 (𝜑 → (∃𝑥𝑦𝜓 ↔ ∃𝑥𝑦𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∃wex 1782 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912 This theorem depends on definitions:  df-bi 210  df-ex 1783 This theorem is referenced by:  3exbidv  1927  4exbidv  1928  cbvex4vw  2050  cbvex4v  2427  ceqsex3v  3463  ceqsex4v  3464  2reu5  3673  opabbidv  5099  copsexgw  5350  copsexg  5351  euotd  5373  elopab  5385  elxpi  5547  relop  5691  dfres3  5829  xpdifid  5998  oprabv  7209  cbvoprab3  7240  elrnmpores  7284  ov6g  7309  omxpenlem  8639  dcomex  9900  ltresr  10593  hashle2prv  13881  fsumcom2  15170  fprodcom2  15379  ispos  17616  fsumvma  25889  1pthon2v  28030  dfconngr1  28065  isconngr  28066  isconngr1  28067  1conngr  28071  conngrv2edg  28072  fusgr2wsp2nb  28211  isacycgr  32616  satfv1  32834  sat1el2xp  32850  elfuns  33759  bj-cbvex4vv  34516  itg2addnclem3  35383  brxrn2  36060  dvhopellsm  38686  diblsmopel  38740  2sbc5g  41486  fundcmpsurinj  44287  ichexmpl1  44347  ichnreuop  44350  ichreuopeq  44351  elsprel  44353  prprelb  44394  reuopreuprim  44404
 Copyright terms: Public domain W3C validator