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

Theorem 2exbidv 1760
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 1758 . 2  |-  ( ph  ->  ( E. y ps  <->  E. y ch ) )
32exbidv 1758 1  |-  ( ph  ->  ( E. x E. y ps  <->  E. x E. y ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   E.wex 1659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748
This theorem depends on definitions:  df-bi 188  df-ex 1660
This theorem is referenced by:  3exbidv  1761  4exbidv  1762  cbvex4v  2086  ceqsex3v  3118  ceqsex4v  3119  2reu5  3277  copsexg  4698  euotd  4713  elopab  4720  elxpi  4861  relop  4996  xpdifid  5276  oprabv  6344  cbvoprab3  6372  elrnmpt2res  6415  ov6g  6439  omxpenlem  7670  dcomex  8866  ltresr  9553  fsumcom2  13802  fprodcom2  14005  ispos  16136  fsumvma  24030  dfconngra1  25270  isconngra  25271  isconngra1  25272  1conngra  25274  is2wlkonot  25462  is2spthonot  25463  2wlkonot  25464  2spthonot  25465  el2wlkonot  25468  el2spthonot  25469  el2spthonot0  25470  el2wlkonotot0  25471  2wlkonot3v  25474  2spthonot3v  25475  usg2wotspth  25483  2pthwlkonot  25484  2spotdisj  25660  usg2spot2nb  25664  dfres3  30212  elfuns  30493  bj-cbvex4vv  31114  itg2addnclem3  31728  dvhopellsm  34423  diblsmopel  34477  2sbc5g  36437
  Copyright terms: Public domain W3C validator