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

Theorem 2exbidv 1778
Description: Formula-building rule for two 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 1776 . 2  |-  ( ph  ->  ( E. y ps  <->  E. y ch ) )
32exbidv 1776 1  |-  ( ph  ->  ( E. x E. y ps  <->  E. x E. y ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   E.wex 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766
This theorem depends on definitions:  df-bi 190  df-ex 1672
This theorem is referenced by:  3exbidv  1779  4exbidv  1780  cbvex4v  2139  ceqsex3v  3074  ceqsex4v  3075  2reu5  3236  copsexg  4687  euotd  4702  elopab  4709  elxpi  4855  relop  4990  xpdifid  5271  oprabv  6358  cbvoprab3  6386  elrnmpt2res  6429  ov6g  6453  omxpenlem  7691  dcomex  8895  ltresr  9582  fsumcom2  13912  fprodcom2  14115  ispos  16270  fsumvma  24220  dfconngra1  25478  isconngra  25479  isconngra1  25480  1conngra  25482  is2wlkonot  25670  is2spthonot  25671  2wlkonot  25672  2spthonot  25673  el2wlkonot  25676  el2spthonot  25677  el2spthonot0  25678  el2wlkonotot0  25679  2wlkonot3v  25682  2spthonot3v  25683  usg2wotspth  25691  2pthwlkonot  25692  2spotdisj  25868  usg2spot2nb  25872  dfres3  30470  elfuns  30753  bj-cbvex4vv  31410  itg2addnclem3  32059  dvhopellsm  34756  diblsmopel  34810  2sbc5g  36837  1pthon2v-av  40041  dfconngr1  40102  isconngr  40103  isconngr1  40104  1conngr  40108
  Copyright terms: Public domain W3C validator