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

Theorem mpgbir 1684
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  |-  ( ph  <->  A. x ps )
mpgbir.2  |-  ps
Assertion
Ref Expression
mpgbir  |-  ph

Proof of Theorem mpgbir
StepHypRef Expression
1 mpgbir.2 . . 3  |-  ps
21ax-gen 1680 . 2  |-  A. x ps
3 mpgbir.1 . 2  |-  ( ph  <->  A. x ps )
42, 3mpbir 214 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189   A.wal 1453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680
This theorem depends on definitions:  df-bi 190
This theorem is referenced by:  nfi  1685  cvjust  2457  eqriv  2459  abbi2i  2577  nfci  2593  abid2f  2629  rgen  2759  ssriv  3448  ss2abi  3513  ssmin  4267  intab  4279  iunab  4338  iinab  4353  sndisj  4408  disjxsn  4410  intid  4672  fr0  4832  relssi  4945  dm0  5067  dmi  5068  onfr  5481  funopabeq  5635  isarep2  5685  opabiotafun  5949  fvopab3ig  5968  opabex  6159  caovmo  6533  ordom  6728  tz7.44lem1  7149  dfsup2  7984  zfregfr  8143  dfom3  8178  trcl  8238  tc2  8252  rankf  8291  rankval4  8364  uniwun  9191  dfnn2  10650  dfuzi  11055  fzodisj  11983  fzouzdisj  11985  cycsubg  16894  efger  17417  ajfuni  26550  funadj  27588  rabexgfGS  28186  abrexdomjm  28190  ballotth  29419  ballotthOLD  29457  bnj1133  29847  dfon3  30708  fnsingle  30735  dfiota3  30739  hftr  30998  bj-abbi2i  31436  bj-rabtrALT  31579  bj-nel0  31586  bj-vjust2  31664  bj-df-v  31665  ismblfin  32026  abrexdom  32102  cllem0  36215  cotrintab  36266  brtrclfv2  36364  snhesn  36427  psshepw  36429  compab  36838  onfrALT  36959  dvcosre  37819  stoweidlem44  37943  alimp-surprise  40792
  Copyright terms: Public domain W3C validator