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 231 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wcel 2108  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795
This theorem depends on definitions:  df-bi 207  df-ral 3062
This theorem is referenced by:  ss2rabi  4077  ssintub  4966  djussxp  5856  dmiin  5964  dfco2  6265  coiun  6276  tron  6407  onxpdisj  6510  epweon  7795  frrlem6  8316  frrlem7  8317  wfrrelOLD  8354  wfrdmssOLD  8355  tfrlem6  8422  oawordeulem  8592  sbthlem1  9123  marypha2lem1  9475  ttrclselem1  9765  rankval4  9907  tcwf  9923  inlresf  9954  inrresf  9956  fin23lem16  10375  fin23lem29  10381  fin23lem30  10382  itunitc  10461  acncc  10480  wfgru  10856  renfdisj  11321  ioomax  13462  iccmax  13463  hashgval2  14417  fsumcom2  15810  fprodcom2  16020  dfphi2  16811  oppccatf  17771  dmcoass  18111  letsr  18638  smndex2dnrinv  18928  efgsf  19747  lssuni  20937  lpival  21334  cnsubdrglem  21436  retos  21636  psr1baslem  22186  istopon  22918  neips  23121  filssufilg  23919  xrhmeo  24977  iscmet3i  25346  ehlbase  25449  ovolge0  25516  unidmvol  25576  resinf1o  26578  divlogrlim  26677  dvloglem  26690  logf1o2  26692  atansssdm  26976  ppiub  27248  bday1s  27876  lrrecse  27975  clwwlkn0  30047  sspval  30742  shintcli  31348  lnopco0i  32023  imaelshi  32077  nmopadjlem  32108  nmoptrii  32113  nmopcoi  32114  nmopcoadji  32120  idleop  32150  hmopidmchi  32170  hmopidmpji  32171  djussxp2  32658  xrsclat  33013  rearchi  33374  dmvlsiga  34130  sxbrsigalem0  34273  dya2iocucvr  34286  eulerpartlemgh  34380  bnj110  34872  subfacp1lem1  35184  erdszelem2  35197  dfon2lem3  35786  filnetlem2  36380  taupi  37324  cnviun  43663  coiun1  43665  comptiunov2i  43719  cotrcltrcl  43738  cotrclrcl  43755  ssrab2f  45122  iooinlbub  45514  stirlinglem14  46102  sssalgen  46350  fvmptrabdm  47305  stgr0  47927  unilbss  48737
  Copyright terms: Public domain W3C validator