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

Theorem 2exbidv 1635
Description: Formula-building rule for 2 existential quantifiers (deduction rule). (Contributed by NM, 1-May-1995.)
Hypothesis
Ref Expression
2albidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
2exbidv  |-  ( ph  ->  ( E. x E. y ps  <->  E. x E. y ch ) )
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    ps( x, y)    ch( x, y)

Proof of Theorem 2exbidv
StepHypRef Expression
1 2albidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21exbidv 1633 . 2  |-  ( ph  ->  ( E. y ps  <->  E. y ch ) )
32exbidv 1633 1  |-  ( ph  ->  ( E. x E. y ps  <->  E. x E. y ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wex 1547
This theorem is referenced by:  3exbidv  1636  4exbidv  1637  cbvex4v  2062  ceqsex3v  2954  ceqsex4v  2955  2reu5  3102  copsexg  4402  euotd  4417  elopab  4422  elxpi  4853  relop  4982  cbvoprab3  6107  ov6g  6170  th3qlem1  6969  omxpenlem  7168  dcomex  8283  ltresr  8971  fsumcom2  12513  ispos  14359  fsumvma  20950  dfconngra1  21611  isconngra  21612  isconngra1  21613  1conngra  21615  fprodcom2  25261  dfres3  25330  itg2addnclem3  26157  2sbc5g  27484  is2wlkonot  28060  is2spthonot  28061  2wlkonot  28062  2spthonot  28063  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  el2wlkonotot0  28069  2wlkonot3v  28072  2spthonot3v  28073  usg2wotspth  28081  2pthwlkonot  28082  2spotdisj  28164  usg2spot2nb  28168  cbvex4vOLD7  29422  dvhopellsm  31600  diblsmopel  31654
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator