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

Theorem mprgbir 2768
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 2763 . 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 1725   A.wral 2697
This theorem is referenced by:  ss2rabi  3417  rabxm  3642  rabnc  3643  ssintub  4060  tron  4596  onxpdisj  4949  djussxp  5010  dmiin  5105  dfco2  5361  coiun  5371  tfrlem6  6635  oawordeulem  6789  sbthlem1  7209  marypha2lem1  7432  rankval4  7785  tcwf  7799  fin23lem16  8207  fin23lem29  8213  fin23lem30  8214  itunitc  8293  acncc  8312  wfgru  8683  renfdisj  9130  ioomax  10977  iccmax  10978  hashgval2  11644  fsumcom2  12550  dfphi2  13155  dmcoass  14213  letsr  14664  efgsf  15353  lssuni  16008  lpival  16308  psr1baslem  16575  cnsubdrglem  16741  istopon  16982  neips  17169  filssufilg  17935  xrhmeo  18963  iscmet3i  19256  ovolge0  19369  resinf1o  20430  divlogrlim  20518  dvloglem  20531  logf1o2  20533  atansssdm  20765  ppiub  20980  sspval  22214  shintcli  22823  lnopco0i  23499  imaelshi  23553  nmopadjlem  23584  nmoptrii  23589  nmopcoi  23590  nmopcoadji  23596  idleop  23626  hmopidmchi  23646  hmopidmpji  23647  retos  24270  dmvlsiga  24504  unidmvol  24576  sxbrsigalem0  24613  dya2iocucvr  24626  subfacp1lem1  24857  erdszelem2  24870  fprodcom2  25300  dfon2lem3  25404  trpredlem1  25497  wfrlem6  25535  wfrlem7  25536  frrlem6  25583  frrlem7  25584  nofulllem5  25653  mblfinlem  26234  filnetlem2  26399  stirlinglem14  27803  bnj110  29166
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555
This theorem depends on definitions:  df-bi 178  df-ral 2702
  Copyright terms: Public domain W3C validator