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

Theorem 2exbidv 1692
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 1690 . 2  |-  ( ph  ->  ( E. y ps  <->  E. y ch ) )
32exbidv 1690 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 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  3exbidv  1693  4exbidv  1694  cbvex4v  2007  ceqsex3v  3153  ceqsex4v  3154  2reu5  3312  copsexg  4732  copsexgOLD  4733  euotd  4748  elopab  4755  elxpi  5015  relop  5153  xpdifid  5435  oprabv  6329  cbvoprab3  6357  elrnmpt2res  6400  ov6g  6424  omxpenlem  7618  dcomex  8827  ltresr  9517  fsumcom2  13552  ispos  15434  fsumvma  23244  dfconngra1  24375  isconngra  24376  isconngra1  24377  1conngra  24379  is2wlkonot  24567  is2spthonot  24568  2wlkonot  24569  2spthonot  24570  el2wlkonot  24573  el2spthonot  24574  el2spthonot0  24575  el2wlkonotot0  24576  2wlkonot3v  24579  2spthonot3v  24580  usg2wotspth  24588  2pthwlkonot  24589  2spotdisj  24766  usg2spot2nb  24770  fprodcom2  28719  dfres3  28793  elfuns  29170  itg2addnclem3  29673  2sbc5g  30929  bj-cbvex4vv  33408  dvhopellsm  35932  diblsmopel  35986
  Copyright terms: Public domain W3C validator