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

Theorem mpgbir 1605
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 1601 . 2  |-  A. x ps
3 mpgbir.1 . 2  |-  ( ph  <->  A. x ps )
42, 3mpbir 209 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   A.wal 1377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  nfi  1606  cvjust  2461  eqriv  2463  abbi2i  2600  nfci  2618  abid2f  2658  abid2fOLD  2659  rgen  2824  ssriv  3508  ss2abi  3572  ssmin  4301  intab  4312  iunab  4371  iinab  4386  sndisj  4439  disjxsn  4441  intid  4705  fr0  4858  onfr  4917  relssi  5094  dm0  5216  dmi  5217  funopabeq  5622  isarep2  5668  opabiotafun  5928  fvopab3ig  5947  opabex  6129  caovmo  6496  ordom  6693  tz7.44lem1  7071  dfsup2  7902  dfsup2OLD  7903  zfregfr  8029  dfom3  8064  trcl  8159  tc2  8173  rankf  8212  rankval4  8285  uniwun  9118  dfnn2  10549  dfuzi  10951  fzodisj  11827  fzouzdisj  11829  cycsubg  16034  efger  16542  ajfuni  25479  funadj  26509  rabexgfGS  27105  abrexdomjm  27107  ballotth  28144  dfon3  29147  fnsingle  29174  dfiota3  29178  hftr  29444  ismblfin  29660  abrexdom  29852  compab  30956  fzssz  31071  dvcosre  31267  stoweidlem44  31372  alimp-surprise  32294  onfrALT  32419  bnj1133  33142  bj-abbi2i  33461  bj-rabtrALT  33597  bj-nel0  33603  bj-df-v  33682  cllem0  36789
  Copyright terms: Public domain W3C validator