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

Theorem mprgbir 2923
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 2918 . 2 𝑥𝐴 𝜓
3 mprgbir.1 . 2 (𝜑 ↔ ∀𝑥𝐴 𝜓)
42, 3mpbir 221 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wcel 1987  wral 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719
This theorem depends on definitions:  df-bi 197  df-ral 2913
This theorem is referenced by:  ss2rabi  3669  rabxm  3941  ssintub  4467  djussxp  5237  dmiin  5339  dfco2  5603  coiun  5614  tron  5715  onxpdisj  5816  wfrrel  7380  wfrdmss  7381  tfrlem6  7438  oawordeulem  7594  sbthlem1  8030  marypha2lem1  8301  rankval4  8690  tcwf  8706  fin23lem16  9117  fin23lem29  9123  fin23lem30  9124  itunitc  9203  acncc  9222  wfgru  9598  renfdisj  10058  ioomax  12206  iccmax  12207  hashgval2  13123  fsumcom2  14452  fsumcom2OLD  14453  fprodcom2  14658  fprodcom2OLD  14659  dfphi2  15422  dmcoass  16656  letsr  17167  efgsf  18082  lssuni  18880  lpival  19185  psr1baslem  19495  cnsubdrglem  19737  retos  19904  istopon  20657  neips  20857  filssufilg  21655  xrhmeo  22685  iscmet3i  23050  ehlbase  23134  ovolge0  23189  unidmvol  23249  resinf1o  24220  divlogrlim  24315  dvloglem  24328  logf1o2  24330  atansssdm  24594  ppiub  24863  sspval  27466  shintcli  28076  lnopco0i  28751  imaelshi  28805  nmopadjlem  28836  nmoptrii  28841  nmopcoi  28842  nmopcoadji  28848  idleop  28878  hmopidmchi  28898  hmopidmpji  28899  xrsclat  29507  rearchi  29669  dmvlsiga  30015  sxbrsigalem0  30156  dya2iocucvr  30169  eulerpartlemgh  30263  bnj110  30689  subfacp1lem1  30922  erdszelem2  30935  dfon2lem3  31444  trpredlem1  31481  frrlem6  31543  frrlem7  31544  filnetlem2  32069  taupi  32841  cnviun  37462  coiun1  37464  comptiunov2i  37518  cotrcltrcl  37537  cotrclrcl  37554  ssrab2f  38824  iooinlbub  39169  stirlinglem14  39641  sssalgen  39890
  Copyright terms: Public domain W3C validator