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

Theorem mprgbir 3068
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 3063 . 2 𝑥𝐴 𝜓
3 mprgbir.1 . 2 (𝜑 ↔ ∀𝑥𝐴 𝜓)
42, 3mpbir 230 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wcel 2107  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798
This theorem depends on definitions:  df-bi 206  df-ral 3062
This theorem is referenced by:  ss2rabi  4035  rabxm  4347  ssintub  4928  djussxp  5802  dmiin  5909  dfco2  6198  coiun  6209  tron  6341  onxpdisj  6444  epweon  7710  frrlem6  8223  frrlem7  8224  wfrrelOLD  8261  wfrdmssOLD  8262  tfrlem6  8329  oawordeulem  8502  sbthlem1  9030  marypha2lem1  9376  ttrclselem1  9666  rankval4  9808  tcwf  9824  inlresf  9855  inrresf  9857  fin23lem16  10276  fin23lem29  10282  fin23lem30  10283  itunitc  10362  acncc  10381  wfgru  10757  renfdisj  11220  ioomax  13345  iccmax  13346  hashgval2  14284  fsumcom2  15664  fprodcom2  15872  dfphi2  16651  oppccatf  17615  dmcoass  17957  letsr  18487  smndex2dnrinv  18730  efgsf  19516  lssuni  20415  lpival  20731  cnsubdrglem  20864  retos  21038  psr1baslem  21572  istopon  22277  neips  22480  filssufilg  23278  xrhmeo  24325  iscmet3i  24692  ehlbase  24795  ovolge0  24861  unidmvol  24921  resinf1o  25908  divlogrlim  26006  dvloglem  26019  logf1o2  26021  atansssdm  26299  ppiub  26568  bday1s  27192  lrrecse  27276  clwwlkn0  29014  sspval  29707  shintcli  30313  lnopco0i  30988  imaelshi  31042  nmopadjlem  31073  nmoptrii  31078  nmopcoi  31079  nmopcoadji  31085  idleop  31115  hmopidmchi  31135  hmopidmpji  31136  djussxp2  31610  xrsclat  31920  rearchi  32185  dmvlsiga  32785  sxbrsigalem0  32928  dya2iocucvr  32941  eulerpartlemgh  33035  bnj110  33527  subfacp1lem1  33830  erdszelem2  33843  dfon2lem3  34416  filnetlem2  34897  taupi  35840  cnviun  42010  coiun1  42012  comptiunov2i  42066  cotrcltrcl  42085  cotrclrcl  42102  ssrab2f  43415  iooinlbub  43825  stirlinglem14  44414  sssalgen  44662  fvmptrabdm  45611  unilbss  46988
  Copyright terms: Public domain W3C validator