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

Theorem mpgbir 1669
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 1665 . 2  |-  A. x ps
3 mpgbir.1 . 2  |-  ( ph  <->  A. x ps )
42, 3mpbir 212 1  |-  ph
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187   A.wal 1435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665
This theorem depends on definitions:  df-bi 188
This theorem is referenced by:  nfi  1670  cvjust  2414  eqriv  2416  abbi2i  2553  nfci  2571  abid2f  2611  abid2fOLD  2612  rgen  2783  ssriv  3465  ss2abi  3530  ssmin  4268  intab  4280  iunab  4339  iinab  4354  sndisj  4409  disjxsn  4411  intid  4671  fr0  4824  relssi  4937  dm0  5059  dmi  5060  onfr  5472  funopabeq  5626  isarep2  5672  opabiotafun  5933  fvopab3ig  5952  opabex  6140  caovmo  6511  ordom  6706  tz7.44lem1  7122  dfsup2  7955  zfregfr  8108  dfom3  8143  trcl  8202  tc2  8216  rankf  8255  rankval4  8328  uniwun  9154  dfnn2  10611  dfuzi  11015  fzodisj  11939  fzouzdisj  11941  cycsubg  16789  efger  17296  ajfuni  26343  funadj  27371  rabexgfGS  27970  abrexdomjm  27974  ballotth  29193  bnj1133  29583  dfon3  30441  fnsingle  30468  dfiota3  30472  hftr  30731  bj-abbi2i  31139  bj-rabtrALT  31281  bj-nel0  31287  bj-df-v  31365  ismblfin  31685  abrexdom  31761  cllem0  35873  brtrclfv2  35962  snhesn  36023  psshepw  36025  compab  36435  onfrALT  36556  dvcosre  37357  stoweidlem44  37478  alimp-surprise  39293
  Copyright terms: Public domain W3C validator