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

Theorem mprgbir 2818
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 2814 . 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 1823   A.wral 2804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623
This theorem depends on definitions:  df-bi 185  df-ral 2809
This theorem is referenced by:  ss2rabi  3568  rabxm  3807  rabnc  3808  ssintub  4289  tron  4890  onxpdisj  5071  djussxp  5137  dmiin  5235  dfco2  5489  coiun  5500  tfrlem6  7043  oawordeulem  7195  sbthlem1  7620  marypha2lem1  7887  rankval4  8276  tcwf  8292  fin23lem16  8706  fin23lem29  8712  fin23lem30  8713  itunitc  8792  acncc  8811  wfgru  9183  renfdisj  9636  ioomax  11602  iccmax  11603  hashgval2  12432  fsumcom2  13674  fprodcom2  13873  dfphi2  14391  dmcoass  15547  letsr  16059  efgsf  16949  lssuni  17784  lpival  18091  psr1baslem  18422  cnsubdrglem  18667  retos  18830  istopon  19596  neips  19784  filssufilg  20581  xrhmeo  21615  iscmet3i  21919  ehlbase  22007  ovolge0  22061  resinf1o  23092  divlogrlim  23187  dvloglem  23200  logf1o2  23202  atansssdm  23464  ppiub  23680  sspval  25837  shintcli  26448  lnopco0i  27124  imaelshi  27178  nmopadjlem  27209  nmoptrii  27214  nmopcoi  27215  nmopcoadji  27221  idleop  27251  hmopidmchi  27271  hmopidmpji  27272  xrsclat  27905  rearchi  28070  dmvlsiga  28362  unidmvol  28440  sxbrsigalem0  28482  dya2iocucvr  28495  eulerpartlemgh  28584  subfacp1lem1  28890  erdszelem2  28903  dfon2lem3  29460  trpredlem1  29553  wfrlem6  29591  wfrlem7  29592  frrlem6  29639  frrlem7  29640  nofulllem5  29709  dvtanlem  30307  filnetlem2  30440  iooinlbub  31776  stirlinglem14  32111  bnj110  34336  taupi  38114  coiun1  38192  cnviun  38193  comptiunov2i  38237  cotrclrcl  38253  cotrcltrcl  38254
  Copyright terms: Public domain W3C validator