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

Theorem 2exbidv 1638
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 1636 . 2  |-  ( ph  ->  ( E. y ps  <->  E. y ch ) )
32exbidv 1636 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 1550
This theorem is referenced by:  3exbidv  1639  4exbidv  1640  cbvex4v  1996  ceqsex3v  2994  ceqsex4v  2995  2reu5  3142  copsexg  4442  euotd  4457  elopab  4462  elxpi  4894  relop  5023  cbvoprab3  6148  ov6g  6211  th3qlem1  7010  omxpenlem  7209  dcomex  8327  ltresr  9015  fsumcom2  12558  ispos  14404  fsumvma  20997  dfconngra1  21658  isconngra  21659  isconngra1  21660  1conngra  21662  fprodcom2  25308  dfres3  25382  elfuns  25760  itg2addnclem3  26258  2sbc5g  27593  oprabv  28085  is2wlkonot  28330  is2spthonot  28331  2wlkonot  28332  2spthonot  28333  el2wlkonot  28336  el2spthonot  28337  el2spthonot0  28338  el2wlkonotot0  28339  2wlkonot3v  28342  2spthonot3v  28343  usg2wotspth  28351  2pthwlkonot  28352  2spotdisj  28450  usg2spot2nb  28454  cbvex4vOLD7  29738  dvhopellsm  31915  diblsmopel  31969
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator