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

Theorem mprgbir 2821
Description: Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)
Hypotheses
Ref Expression
mprgbir.1
mprgbir.2
Assertion
Ref Expression
mprgbir

Proof of Theorem mprgbir
StepHypRef Expression
1 mprgbir.2 . . 3
21rgen 2817 . 2
3 mprgbir.1 . 2
42, 3mpbir 209 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  e.wcel 1818  A.wral 2807
This theorem is referenced by:  ss2rabi  3581  rabxm  3808  rabnc  3809  ssintub  4304  tron  4906  onxpdisj  5088  djussxp  5153  dmiin  5251  dfco2  5511  coiun  5522  tfrlem6  7070  oawordeulem  7222  sbthlem1  7647  marypha2lem1  7915  rankval4  8306  tcwf  8322  fin23lem16  8736  fin23lem29  8742  fin23lem30  8743  itunitc  8822  acncc  8841  wfgru  9215  renfdisj  9668  ioomax  11628  iccmax  11629  hashgval2  12446  fsumcom2  13589  fprodcom2  13788  dfphi2  14304  dmcoass  15393  letsr  15857  efgsf  16747  lssuni  17586  lpival  17893  psr1baslem  18224  cnsubdrglem  18469  retos  18654  istopon  19426  neips  19614  filssufilg  20412  xrhmeo  21446  iscmet3i  21750  ehlbase  21838  ovolge0  21892  resinf1o  22923  divlogrlim  23016  dvloglem  23029  logf1o2  23031  atansssdm  23264  ppiub  23479  sspval  25636  shintcli  26247  lnopco0i  26923  imaelshi  26977  nmopadjlem  27008  nmoptrii  27013  nmopcoi  27014  nmopcoadji  27020  idleop  27050  hmopidmchi  27070  hmopidmpji  27071  xrsclat  27668  rearchi  27832  dmvlsiga  28129  unidmvol  28200  sxbrsigalem0  28242  dya2iocucvr  28255  eulerpartlemgh  28317  subfacp1lem1  28623  erdszelem2  28636  dfon2lem3  29217  trpredlem1  29310  wfrlem6  29348  wfrlem7  29349  frrlem6  29396  frrlem7  29397  nofulllem5  29466  dvtanlem  30064  filnetlem2  30197  iooinlbub  31534  stirlinglem14  31869  bnj110  33916  taupi  37698
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618
This theorem depends on definitions:  df-bi 185  df-ral 2812
  Copyright terms: Public domain W3C validator