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

Theorem 2exbidv 1682
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 1680 . 2  |-  ( ph  ->  ( E. y ps  <->  E. y ch ) )
32exbidv 1680 1  |-  ( ph  ->  ( E. x E. y ps  <->  E. x E. y ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wex 1586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670
This theorem depends on definitions:  df-bi 185  df-ex 1587
This theorem is referenced by:  3exbidv  1683  4exbidv  1684  cbvex4v  1982  ceqsex3v  3027  ceqsex4v  3028  2reu5  3182  copsexg  4591  copsexgOLD  4592  euotd  4607  elopab  4612  elxpi  4871  relop  5005  xpdifid  5281  cbvoprab3  6177  elrnmpt2res  6219  ov6g  6243  th3qlem1  7221  omxpenlem  7427  dcomex  8631  ltresr  9322  fsumcom2  13256  ispos  15132  fsumvma  22567  dfconngra1  23572  isconngra  23573  isconngra1  23574  1conngra  23576  fprodcom2  27510  dfres3  27584  elfuns  27961  itg2addnclem3  28464  2sbc5g  29689  oprabv  30176  is2wlkonot  30401  is2spthonot  30402  2wlkonot  30403  2spthonot  30404  el2wlkonot  30407  el2spthonot  30408  el2spthonot0  30409  el2wlkonotot0  30410  2wlkonot3v  30413  2spthonot3v  30414  usg2wotspth  30422  2pthwlkonot  30423  2spotdisj  30673  usg2spot2nb  30677  bj-cbvex4vv  32263  dvhopellsm  34781  diblsmopel  34835
  Copyright terms: Public domain W3C validator