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

Theorem mpgbir 1843
Description: Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.)
Hypotheses
Ref Expression
mpgbir.1 (𝜑 ↔ ∀𝑥𝜓)
mpgbir.2 𝜓
Assertion
Ref Expression
mpgbir 𝜑

Proof of Theorem mpgbir
StepHypRef Expression
1 mpgbir.2 . . 3 𝜓
21ax-gen 1839 . 2 𝑥𝜓
3 mpgbir.1 . 2 (𝜑 ↔ ∀𝑥𝜓)
42, 3mpbir 223 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 198  wal 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839
This theorem depends on definitions:  df-bi 199
This theorem is referenced by:  cvjust  2772  cvjustOLD  2773  eqriv  2775  abbi2iOLD  2901  nfci  2922  abid2f  2965  rgen  3104  rabeqc  3570  ssriv  3825  ss2abi  3895  nel0  4160  rab0  4186  abf  4204  ssmin  4729  intab  4740  iunab  4799  iinab  4814  sndisj  4878  disjxsn  4880  intid  5158  fr0  5334  relssi  5458  dmi  5585  onfr  6015  funopabeq  6171  isarep2  6223  opabiotafun  6519  fvopab3ig  6538  opabex  6755  caovmo  7148  ordom  7352  tz7.44lem1  7784  dfsup2  8638  zfregfr  8798  dfom3  8841  trcl  8901  tc2  8915  rankf  8954  rankval4  9027  uniwun  9897  dfnn2  11389  dfuzi  11820  fzodisj  12821  fzodisjsn  12825  cycsubg  18006  efger  18515  ajfuni  28287  funadj  29317  rabexgfGS  29902  abrexdomjm  29907  ballotth  31198  bnj1133  31656  dfon3  32588  fnsingle  32615  dfiota3  32619  hftr  32878  bj-abbi2i  33353  bj-rabtrALT  33501  bj-df-v  33588  ismblfin  34076  abrexdom  34150  cllem0  38828  cotrintab  38878  brtrclfv2  38976  snhesn  39036  psshepw  39038  k0004val0  39408  compab  39600  onfrALT  39709  dvcosre  41054  alimp-surprise  43632
  Copyright terms: Public domain W3C validator