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

Theorem mprgbir 2784
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 2779 . 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 1756   A.wral 2713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591
This theorem depends on definitions:  df-bi 185  df-ral 2718
This theorem is referenced by:  ss2rabi  3432  rabxm  3658  rabnc  3659  ssintub  4144  tron  4740  onxpdisj  4918  djussxp  4983  dmiin  5081  dfco2  5335  coiun  5345  tfrlem6  6839  oawordeulem  6991  sbthlem1  7419  marypha2lem1  7683  rankval4  8072  tcwf  8088  fin23lem16  8502  fin23lem29  8508  fin23lem30  8509  itunitc  8588  acncc  8607  wfgru  8981  renfdisj  9435  ioomax  11368  iccmax  11369  hashgval2  12139  fsumcom2  13239  dfphi2  13847  dmcoass  14932  letsr  15395  efgsf  16224  lssuni  17019  lpival  17325  psr1baslem  17639  cnsubdrglem  17862  retos  18046  istopon  18528  neips  18715  filssufilg  19482  xrhmeo  20516  iscmet3i  20820  ovolge0  20962  resinf1o  21990  divlogrlim  22078  dvloglem  22091  logf1o2  22093  atansssdm  22326  ppiub  22541  sspval  24119  shintcli  24730  lnopco0i  25406  imaelshi  25460  nmopadjlem  25491  nmoptrii  25496  nmopcoi  25497  nmopcoadji  25503  idleop  25533  hmopidmchi  25553  hmopidmpji  25554  xrsclat  26139  dmvlsiga  26570  unidmvol  26642  sxbrsigalem0  26684  dya2iocucvr  26697  eulerpartlemgh  26759  subfacp1lem1  27065  erdszelem2  27078  fprodcom2  27493  dfon2lem3  27596  trpredlem1  27689  wfrlem6  27727  wfrlem7  27728  frrlem6  27775  frrlem7  27776  nofulllem5  27845  dvtanlem  28438  filnetlem2  28597  stirlinglem14  29879  bnj110  31848  taupi  35614
  Copyright terms: Public domain W3C validator