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

Theorem mprgbir 3065
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 3060 . 2 𝑥𝐴 𝜓
3 mprgbir.1 . 2 (𝜑 ↔ ∀𝑥𝐴 𝜓)
42, 3mpbir 221 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wcel 2139  wral 3050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871
This theorem depends on definitions:  df-bi 197  df-ral 3055
This theorem is referenced by:  ss2rabi  3825  rabxm  4104  ssintub  4647  djussxp  5423  dmiin  5524  dfco2  5795  coiun  5806  tron  5907  onxpdisj  6008  wfrrel  7589  wfrdmss  7590  tfrlem6  7647  oawordeulem  7803  sbthlem1  8235  marypha2lem1  8506  rankval4  8903  tcwf  8919  fin23lem16  9349  fin23lem29  9355  fin23lem30  9356  itunitc  9435  acncc  9454  wfgru  9830  renfdisj  10290  ioomax  12441  iccmax  12442  hashgval2  13359  fsumcom2  14704  fsumcom2OLD  14705  fprodcom2  14913  fprodcom2OLD  14914  dfphi2  15681  dmcoass  16917  letsr  17428  efgsf  18342  lssuni  19142  lpival  19447  psr1baslem  19757  cnsubdrglem  19999  retos  20166  istopon  20919  neips  21119  filssufilg  21916  xrhmeo  22946  iscmet3i  23310  ehlbase  23394  ovolge0  23449  unidmvol  23509  resinf1o  24481  divlogrlim  24580  dvloglem  24593  logf1o2  24595  atansssdm  24859  ppiub  25128  clwwlkn0  27155  sspval  27887  shintcli  28497  lnopco0i  29172  imaelshi  29226  nmopadjlem  29257  nmoptrii  29262  nmopcoi  29263  nmopcoadji  29269  idleop  29299  hmopidmchi  29319  hmopidmpji  29320  xrsclat  29989  rearchi  30151  dmvlsiga  30501  sxbrsigalem0  30642  dya2iocucvr  30655  eulerpartlemgh  30749  bnj110  31235  subfacp1lem1  31468  erdszelem2  31481  dfon2lem3  31995  trpredlem1  32032  frrlem6  32095  frrlem7  32096  filnetlem2  32680  taupi  33480  cnfinltrel  33552  cnviun  38444  coiun1  38446  comptiunov2i  38500  cotrcltrcl  38519  cotrclrcl  38536  ssrab2f  39799  iooinlbub  40226  stirlinglem14  40807  sssalgen  41056  fvmptrabdm  41817
  Copyright terms: Public domain W3C validator