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

Theorem mprgbir 2626
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 2621 . 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 1696   A.wral 2556
This theorem is referenced by:  ss2rabi  3268  rabxm  3490  rabnc  3491  ssintub  3896  tron  4431  onxpdisj  4785  djussxp  4845  dmiin  4938  dfco2  5188  coiun  5198  tfrlem6  6414  oawordeulem  6568  sbthlem1  6987  marypha2lem1  7204  rankval4  7555  tcwf  7569  fin23lem16  7977  fin23lem29  7983  fin23lem30  7984  itunitc  8063  acncc  8082  wfgru  8454  renfdisj  8901  ioomax  10740  iccmax  10741  hashgval2  11376  fsumcom2  12253  dfphi2  12858  letsr  14365  efgsf  15054  lssuni  15713  lpival  16013  psr1baslem  16280  cnsubdrglem  16438  istopon  16679  neips  16866  filssufilg  17622  xrhmeo  18460  iscmet3i  18753  ovolge0  18856  resinf1o  19914  divlogrlim  19998  dvloglem  20011  logf1o2  20013  atansssdm  20245  ppiub  20459  sspval  21315  shintcli  21924  lnopco0i  22600  imaelshi  22654  nmopadjlem  22685  nmoptrii  22690  nmopcoi  22691  nmopcoadji  22697  idleop  22727  hmopidmchi  22747  hmopidmpji  22748  unidmvol  23210  subfacp1lem1  23725  erdszelem2  23738  dfon2lem3  24212  trpredlem1  24301  wfrlem6  24332  wfrlem7  24333  frrlem6  24361  frrlem7  24362  nofulllem5  24431  inposet  25381  intopcoaconlem3  25642  filnetlem2  26431  bnj110  29206
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536
This theorem depends on definitions:  df-bi 177  df-ral 2561
  Copyright terms: Public domain W3C validator