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

Theorem mprgbir 2807
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 2803 . 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 1804   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605
This theorem depends on definitions:  df-bi 185  df-ral 2798
This theorem is referenced by:  ss2rabi  3567  rabxm  3794  rabnc  3795  ssintub  4289  tron  4891  onxpdisj  5073  djussxp  5138  dmiin  5236  dfco2  5496  coiun  5507  tfrlem6  7053  oawordeulem  7205  sbthlem1  7629  marypha2lem1  7897  rankval4  8288  tcwf  8304  fin23lem16  8718  fin23lem29  8724  fin23lem30  8725  itunitc  8804  acncc  8823  wfgru  9197  renfdisj  9650  ioomax  11610  iccmax  11611  hashgval2  12428  fsumcom2  13571  fprodcom2  13770  dfphi2  14286  dmcoass  15372  letsr  15836  efgsf  16726  lssuni  17565  lpival  17872  psr1baslem  18203  cnsubdrglem  18448  retos  18632  istopon  19404  neips  19592  filssufilg  20390  xrhmeo  21424  iscmet3i  21728  ehlbase  21816  ovolge0  21870  resinf1o  22901  divlogrlim  22994  dvloglem  23007  logf1o2  23009  atansssdm  23242  ppiub  23457  sspval  25614  shintcli  26225  lnopco0i  26901  imaelshi  26955  nmopadjlem  26986  nmoptrii  26991  nmopcoi  26992  nmopcoadji  26998  idleop  27028  hmopidmchi  27048  hmopidmpji  27049  xrsclat  27646  rearchi  27810  dmvlsiga  28107  unidmvol  28178  sxbrsigalem0  28220  dya2iocucvr  28233  eulerpartlemgh  28295  subfacp1lem1  28601  erdszelem2  28614  dfon2lem3  29193  trpredlem1  29286  wfrlem6  29324  wfrlem7  29325  frrlem6  29372  frrlem7  29373  nofulllem5  29442  dvtanlem  30040  filnetlem2  30173  iooinlbub  31488  stirlinglem14  31823  bnj110  33784  taupi  37573
  Copyright terms: Public domain W3C validator