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

Theorem mprgbir 2712
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 2707 . 2  |-  A. x  e.  A  ps
3 mprgbir.1 . 2  |-  ( ph  <->  A. x  e.  A  ps )
42, 3mpbir 201 1  |-  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    e. wcel 1717   A.wral 2642
This theorem is referenced by:  ss2rabi  3361  rabxm  3586  rabnc  3587  ssintub  4003  tron  4538  onxpdisj  4890  djussxp  4951  dmiin  5046  dfco2  5302  coiun  5312  tfrlem6  6572  oawordeulem  6726  sbthlem1  7146  marypha2lem1  7368  rankval4  7719  tcwf  7733  fin23lem16  8141  fin23lem29  8147  fin23lem30  8148  itunitc  8227  acncc  8246  wfgru  8617  renfdisj  9064  ioomax  10910  iccmax  10911  hashgval2  11572  fsumcom2  12478  dfphi2  13083  dmcoass  14141  letsr  14592  efgsf  15281  lssuni  15936  lpival  16236  psr1baslem  16503  cnsubdrglem  16665  istopon  16906  neips  17093  filssufilg  17857  xrhmeo  18835  iscmet3i  19128  ovolge0  19237  resinf1o  20298  divlogrlim  20386  dvloglem  20399  logf1o2  20401  atansssdm  20633  ppiub  20848  sspval  22063  shintcli  22672  lnopco0i  23348  imaelshi  23402  nmopadjlem  23433  nmoptrii  23438  nmopcoi  23439  nmopcoadji  23445  idleop  23475  hmopidmchi  23495  hmopidmpji  23496  retos  24087  dmvlsiga  24301  unidmvol  24371  sxbrsigalem0  24408  dya2iocucvr  24421  subfacp1lem1  24637  erdszelem2  24650  dfon2lem3  25158  trpredlem1  25247  wfrlem6  25278  wfrlem7  25279  frrlem6  25307  frrlem7  25308  nofulllem5  25377  filnetlem2  26092  stirlinglem14  27497  bnj110  28560
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552
This theorem depends on definitions:  df-bi 178  df-ral 2647
  Copyright terms: Public domain W3C validator