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

Theorem 2exbidv 1769
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 1767 . 2  |-  ( ph  ->  ( E. y ps  <->  E. y ch ) )
32exbidv 1767 1  |-  ( ph  ->  ( E. x E. y ps  <->  E. x E. y ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188   E.wex 1662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757
This theorem depends on definitions:  df-bi 189  df-ex 1663
This theorem is referenced by:  3exbidv  1770  4exbidv  1771  cbvex4v  2125  ceqsex3v  3087  ceqsex4v  3088  2reu5  3247  copsexg  4686  euotd  4701  elopab  4708  elxpi  4849  relop  4984  xpdifid  5264  oprabv  6336  cbvoprab3  6364  elrnmpt2res  6407  ov6g  6431  omxpenlem  7670  dcomex  8874  ltresr  9561  fsumcom2  13828  fprodcom2  14031  ispos  16185  fsumvma  24134  dfconngra1  25392  isconngra  25393  isconngra1  25394  1conngra  25396  is2wlkonot  25584  is2spthonot  25585  2wlkonot  25586  2spthonot  25587  el2wlkonot  25590  el2spthonot  25591  el2spthonot0  25592  el2wlkonotot0  25593  2wlkonot3v  25596  2spthonot3v  25597  usg2wotspth  25605  2pthwlkonot  25606  2spotdisj  25782  usg2spot2nb  25786  dfres3  30392  elfuns  30675  bj-cbvex4vv  31337  itg2addnclem3  31988  dvhopellsm  34679  diblsmopel  34733  2sbc5g  36761
  Copyright terms: Public domain W3C validator