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

Theorem mpgbir 1715
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 1711 . 2 𝑥𝜓
3 mpgbir.1 . 2 (𝜑 ↔ ∀𝑥𝜓)
42, 3mpbir 219 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 194  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711
This theorem depends on definitions:  df-bi 195
This theorem is referenced by:  nfiOLD  1723  cvjust  2600  eqriv  2602  abbi2i  2720  nfci  2736  abid2f  2772  rgen  2901  ssriv  3567  ss2abi  3632  rab0  3904  abf  3925  ssmin  4421  intab  4432  iunab  4492  iinab  4507  sndisj  4564  disjxsn  4566  intid  4843  fr0  5003  relssi  5119  dm0  5243  dmi  5244  onfr  5662  funopabeq  5820  isarep2  5874  opabiotafun  6150  fvopab3ig  6169  opabex  6362  caovmo  6742  ordom  6939  tz7.44lem1  7361  dfsup2  8206  zfregfr  8365  dfom3  8400  trcl  8460  tc2  8474  rankf  8513  rankval4  8586  uniwun  9414  dfnn2  10876  dfuzi  11296  fzodisj  12322  fzouzdisj  12324  fzodisjsn  12325  cycsubg  17387  efger  17896  ajfuni  26901  funadj  27931  rabexgfGS  28527  abrexdomjm  28531  ballotth  29728  bnj1133  30113  dfon3  30971  fnsingle  30998  dfiota3  31002  hftr  31261  bj-abbi2i  31773  bj-rabtrALT  31918  bj-nel0  31927  bj-df-v  32006  ismblfin  32419  abrexdom  32494  cllem0  36689  cotrintab  36739  brtrclfv2  36837  snhesn  36899  psshepw  36901  k0004val0  37271  compab  37465  onfrALT  37584  dvcosre  38599  stoweidlem44  38737  alimp-surprise  42294
  Copyright terms: Public domain W3C validator