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

Theorem mprgbir 2911
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 2906 . 2 𝑥𝐴 𝜓
3 mprgbir.1 . 2 (𝜑 ↔ ∀𝑥𝐴 𝜓)
42, 3mpbir 220 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713
This theorem depends on definitions:  df-bi 196  df-ral 2901
This theorem is referenced by:  ss2rabi  3647  rabxm  3915  ssintub  4430  djussxp  5189  dmiin  5290  dfco2  5551  coiun  5562  tron  5663  onxpdisj  5764  wfrrel  7307  wfrdmss  7308  tfrlem6  7365  oawordeulem  7521  sbthlem1  7955  marypha2lem1  8224  rankval4  8613  tcwf  8629  fin23lem16  9040  fin23lem29  9046  fin23lem30  9047  itunitc  9126  acncc  9145  wfgru  9517  renfdisj  9977  ioomax  12119  iccmax  12120  hashgval2  13028  fsumcom2  14347  fsumcom2OLD  14348  fprodcom2  14553  fprodcom2OLD  14554  dfphi2  15317  dmcoass  16539  letsr  17050  efgsf  17965  lssuni  18761  lpival  19066  psr1baslem  19376  cnsubdrglem  19616  retos  19783  istopon  20540  neips  20727  filssufilg  21525  xrhmeo  22553  iscmet3i  22918  ehlbase  23002  ovolge0  23056  unidmvol  23116  resinf1o  24086  divlogrlim  24181  dvloglem  24194  logf1o2  24196  atansssdm  24460  ppiub  24729  sspval  26962  shintcli  27572  lnopco0i  28247  imaelshi  28301  nmopadjlem  28332  nmoptrii  28337  nmopcoi  28338  nmopcoadji  28344  idleop  28374  hmopidmchi  28394  hmopidmpji  28395  xrsclat  29011  rearchi  29173  dmvlsiga  29519  sxbrsigalem0  29660  dya2iocucvr  29673  eulerpartlemgh  29767  bnj110  30182  subfacp1lem1  30415  erdszelem2  30428  dfon2lem3  30934  trpredlem1  30971  frrlem6  31033  frrlem7  31034  nofulllem5  31105  filnetlem2  31544  taupi  32346  cnviun  36961  coiun1  36963  comptiunov2i  37017  cotrcltrcl  37036  cotrclrcl  37053  iooinlbub  38570  stirlinglem14  38980  sssalgen  39229
  Copyright terms: Public domain W3C validator