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

Theorem mprgbir 2771
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 2766 . 2  |-  A. x  e.  A  ps
3 mprgbir.1 . 2  |-  ( ph  <->  A. x  e.  A  ps )
42, 3mpbir 214 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    e. wcel 1904   A.wral 2756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677
This theorem depends on definitions:  df-bi 190  df-ral 2761
This theorem is referenced by:  ss2rabi  3497  rabxm  3758  rabnc  3759  ssintub  4244  djussxp  4985  dmiin  5084  dfco2  5341  coiun  5352  tron  5453  onxpdisj  5549  wfrrel  7059  wfrdmss  7060  tfrlem6  7118  oawordeulem  7273  sbthlem1  7700  marypha2lem1  7967  rankval4  8356  tcwf  8372  fin23lem16  8783  fin23lem29  8789  fin23lem30  8790  itunitc  8869  acncc  8888  wfgru  9259  renfdisj  9712  ioomax  11734  iccmax  11735  hashgval2  12595  fsumcom2  13912  fprodcom2  14115  dfphi2  14801  dmcoass  16039  letsr  16551  efgsf  17457  lssuni  18241  lpival  18546  psr1baslem  18855  cnsubdrglem  19096  retos  19263  istopon  20017  neips  20206  filssufilg  21004  xrhmeo  22052  iscmet3i  22359  ehlbase  22443  ovolge0  22512  unidmvol  22573  resinf1o  23564  divlogrlim  23659  dvloglem  23672  logf1o2  23674  atansssdm  23938  ppiub  24211  sspval  26443  shintcli  27063  lnopco0i  27738  imaelshi  27792  nmopadjlem  27823  nmoptrii  27828  nmopcoi  27829  nmopcoadji  27835  idleop  27865  hmopidmchi  27885  hmopidmpji  27886  xrsclat  28517  rearchi  28679  dmvlsiga  29025  sxbrsigalem0  29166  dya2iocucvr  29179  eulerpartlemgh  29284  bnj110  29741  subfacp1lem1  29974  erdszelem2  29987  dfon2lem3  30502  trpredlem1  30539  frrlem6  30594  frrlem7  30595  nofulllem5  30666  filnetlem2  31106  taupi  31794  dvtanlemOLD  32055  cnviun  36313  coiun1  36315  comptiunov2i  36369  cotrcltrcl  36388  cotrclrcl  36405  iooinlbub  37694  stirlinglem14  38061  sssalgen  38306
  Copyright terms: Public domain W3C validator