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

Theorem mprgbir 3150
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 3145 . 2 𝑥𝐴 𝜓
3 mprgbir.1 . 2 (𝜑 ↔ ∀𝑥𝐴 𝜓)
42, 3mpbir 232 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wcel 2105  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787
This theorem depends on definitions:  df-bi 208  df-ral 3140
This theorem is referenced by:  ss2rabi  4050  rabxm  4337  ssintub  4885  djussxp  5709  dmiin  5818  dfco2  6091  coiun  6102  tron  6207  onxpdisj  6303  wfrrel  7949  wfrdmss  7950  tfrlem6  8007  oawordeulem  8169  sbthlem1  8615  marypha2lem1  8887  rankval4  9284  tcwf  9300  inlresf  9331  inrresf  9333  fin23lem16  9745  fin23lem29  9751  fin23lem30  9752  itunitc  9831  acncc  9850  wfgru  10226  renfdisj  10689  ioomax  12799  iccmax  12800  hashgval2  13727  fsumcom2  15117  fprodcom2  15326  dfphi2  16099  dmcoass  17314  letsr  17825  efgsf  18784  lssuni  19640  lpival  19946  psr1baslem  20281  cnsubdrglem  20524  retos  20690  istopon  21448  neips  21649  filssufilg  22447  xrhmeo  23477  iscmet3i  23842  ehlbase  23945  ovolge0  24009  unidmvol  24069  resinf1o  25047  divlogrlim  25145  dvloglem  25158  logf1o2  25160  atansssdm  25438  ppiub  25707  clwwlkn0  27733  sspval  28427  shintcli  29033  lnopco0i  29708  imaelshi  29762  nmopadjlem  29793  nmoptrii  29798  nmopcoi  29799  nmopcoadji  29805  idleop  29835  hmopidmchi  29855  hmopidmpji  29856  xrsclat  30594  rearchi  30842  dmvlsiga  31287  sxbrsigalem0  31428  dya2iocucvr  31441  eulerpartlemgh  31535  bnj110  32029  subfacp1lem1  32323  erdszelem2  32336  dfon2lem3  32927  trpredlem1  32963  frrlem6  33025  frrlem7  33026  filnetlem2  33624  taupi  34486  cnviun  39873  coiun1  39875  comptiunov2i  39929  cotrcltrcl  39948  cotrclrcl  39965  ssrab2f  41260  iooinlbub  41652  stirlinglem14  42249  sssalgen  42495  fvmptrabdm  43369  smndex2dnrinv  44015
  Copyright terms: Public domain W3C validator