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

Theorem mprgbir 2613
Description: Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)
Hypotheses
Ref Expression
mprgbir.1  |-  ( ph  <->  A. x  e.  A  ps )
mprgbir.2  |-  ( x  e.  A  ->  ps )
Assertion
Ref Expression
mprgbir  |-  ph

Proof of Theorem mprgbir
StepHypRef Expression
1 mprgbir.2 . . 3  |-  ( x  e.  A  ->  ps )
21rgen 2608 . 2  |-  A. x  e.  A  ps
3 mprgbir.1 . 2  |-  ( ph  <->  A. x  e.  A  ps )
42, 3mpbir 200 1  |-  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    e. wcel 1684   A.wral 2543
This theorem is referenced by:  ss2rabi  3255  rabxm  3477  rabnc  3478  ssintub  3880  tron  4415  onxpdisj  4769  djussxp  4829  dmiin  4922  dfco2  5172  coiun  5182  tfrlem6  6398  oawordeulem  6552  sbthlem1  6971  marypha2lem1  7188  rankval4  7539  tcwf  7553  fin23lem16  7961  fin23lem29  7967  fin23lem30  7968  itunitc  8047  acncc  8066  wfgru  8438  renfdisj  8885  ioomax  10724  iccmax  10725  hashgval2  11360  fsumcom2  12237  dfphi2  12842  letsr  14349  efgsf  15038  lssuni  15697  lpival  15997  psr1baslem  16264  cnsubdrglem  16422  istopon  16663  neips  16850  filssufilg  17606  xrhmeo  18444  iscmet3i  18737  ovolge0  18840  resinf1o  19898  divlogrlim  19982  dvloglem  19995  logf1o2  19997  atansssdm  20229  ppiub  20443  sspval  21299  shintcli  21908  lnopco0i  22584  imaelshi  22638  nmopadjlem  22669  nmoptrii  22674  nmopcoi  22675  nmopcoadji  22681  idleop  22711  hmopidmchi  22731  hmopidmpji  22732  unidmvol  23195  subfacp1lem1  23710  erdszelem2  23723  dfon2lem3  24141  trpredlem1  24230  wfrlem6  24261  wfrlem7  24262  frrlem6  24290  frrlem7  24291  nofulllem5  24360  inposet  25278  intopcoaconlem3  25539  filnetlem2  26328  bnj110  28890
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533
This theorem depends on definitions:  df-bi 177  df-ral 2548
  Copyright terms: Public domain W3C validator