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

Theorem mprgbir 2828
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 2824 . 2  |-  A. x  e.  A  ps
3 mprgbir.1 . 2  |-  ( ph  <->  A. x  e.  A  ps )
42, 3mpbir 209 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601
This theorem depends on definitions:  df-bi 185  df-ral 2819
This theorem is referenced by:  ss2rabi  3582  rabxm  3808  rabnc  3809  ssintub  4300  tron  4901  onxpdisj  5083  djussxp  5148  dmiin  5246  dfco2  5506  coiun  5517  tfrlem6  7051  oawordeulem  7203  sbthlem1  7627  marypha2lem1  7895  rankval4  8285  tcwf  8301  fin23lem16  8715  fin23lem29  8721  fin23lem30  8722  itunitc  8801  acncc  8820  wfgru  9194  renfdisj  9647  ioomax  11599  iccmax  11600  hashgval2  12414  fsumcom2  13552  dfphi2  14163  dmcoass  15251  letsr  15714  efgsf  16553  lssuni  17386  lpival  17692  psr1baslem  18023  cnsubdrglem  18265  retos  18449  istopon  19221  neips  19408  filssufilg  20175  xrhmeo  21209  iscmet3i  21513  ovolge0  21655  resinf1o  22684  divlogrlim  22772  dvloglem  22785  logf1o2  22787  atansssdm  23020  ppiub  23235  sspval  25340  shintcli  25951  lnopco0i  26627  imaelshi  26681  nmopadjlem  26712  nmoptrii  26717  nmopcoi  26718  nmopcoadji  26724  idleop  26754  hmopidmchi  26774  hmopidmpji  26775  xrsclat  27358  dmvlsiga  27797  unidmvol  27868  sxbrsigalem0  27910  dya2iocucvr  27923  eulerpartlemgh  27985  subfacp1lem1  28291  erdszelem2  28304  fprodcom2  28719  dfon2lem3  28822  trpredlem1  28915  wfrlem6  28953  wfrlem7  28954  frrlem6  29001  frrlem7  29002  nofulllem5  29071  dvtanlem  29669  filnetlem2  29828  stirlinglem14  31415  bnj110  33013  taupi  36787
  Copyright terms: Public domain W3C validator