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

Theorem mprgbir 2789
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 2785 . 2  |-  A. x  e.  A  ps
3 mprgbir.1 . 2  |-  ( ph  <->  A. x  e.  A  ps )
42, 3mpbir 212 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    e. wcel 1868   A.wral 2775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665
This theorem depends on definitions:  df-bi 188  df-ral 2780
This theorem is referenced by:  ss2rabi  3543  rabxm  3785  rabnc  3786  ssintub  4270  djussxp  4995  dmiin  5093  dfco2  5349  coiun  5360  tron  5461  onxpdisj  5557  wfrrel  7045  wfrdmss  7046  tfrlem6  7104  oawordeulem  7259  sbthlem1  7684  marypha2lem1  7951  rankval4  8339  tcwf  8355  fin23lem16  8765  fin23lem29  8771  fin23lem30  8772  itunitc  8851  acncc  8870  wfgru  9241  renfdisj  9694  ioomax  11709  iccmax  11710  hashgval2  12556  fsumcom2  13820  fprodcom2  14023  dfphi2  14707  dmcoass  15946  letsr  16458  efgsf  17364  lssuni  18148  lpival  18454  psr1baslem  18763  cnsubdrglem  19004  retos  19170  istopon  19924  neips  20113  filssufilg  20910  xrhmeo  21958  iscmet3i  22265  ehlbase  22349  ovolge0  22418  resinf1o  23469  divlogrlim  23564  dvloglem  23577  logf1o2  23579  atansssdm  23843  ppiub  24116  sspval  26345  shintcli  26965  lnopco0i  27640  imaelshi  27694  nmopadjlem  27725  nmoptrii  27730  nmopcoi  27731  nmopcoadji  27737  idleop  27767  hmopidmchi  27787  hmopidmpji  27788  xrsclat  28434  rearchi  28598  dmvlsiga  28944  unidmvol  29044  sxbrsigalem0  29086  dya2iocucvr  29099  eulerpartlemgh  29204  bnj110  29662  subfacp1lem1  29895  erdszelem2  29908  dfon2lem3  30423  trpredlem1  30460  frrlem6  30515  frrlem7  30516  nofulllem5  30585  filnetlem2  31025  taupi  31673  dvtanlemOLD  31902  cnviun  36099  coiun1  36101  comptiunov2i  36155  cotrcltrcl  36174  cotrclrcl  36191  iooinlbub  37426  stirlinglem14  37766
  Copyright terms: Public domain W3C validator