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

Theorem mpgbir 1623
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 1619 . 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 1393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  nfi  1624  cvjust  2451  eqriv  2453  abbi2i  2590  nfci  2608  abid2f  2648  abid2fOLD  2649  rgen  2817  ssriv  3503  ss2abi  3568  ssmin  4307  intab  4319  iunab  4378  iinab  4393  sndisj  4448  disjxsn  4450  intid  4714  fr0  4867  onfr  4926  relssi  5103  dm0  5226  dmi  5227  funopabeq  5628  isarep2  5674  opabiotafun  5934  fvopab3ig  5953  opabex  6142  caovmo  6511  ordom  6708  tz7.44lem1  7089  dfsup2  7920  dfsup2OLD  7921  zfregfr  8046  dfom3  8081  trcl  8176  tc2  8190  rankf  8229  rankval4  8302  uniwun  9135  dfnn2  10569  dfuzi  10974  fzodisj  11858  fzouzdisj  11860  cycsubg  16356  efger  16863  ajfuni  25902  funadj  26932  rabexgfGS  27529  abrexdomjm  27533  ballotth  28673  dfon3  29747  fnsingle  29774  dfiota3  29778  hftr  30044  ismblfin  30260  abrexdom  30426  compab  31554  dvcosre  31909  stoweidlem44  32029  alimp-surprise  33339  onfrALT  33464  bnj1133  34188  bj-abbi2i  34505  bj-rabtrALT  34641  bj-nel0  34647  bj-df-v  34726  cllem0  37911  trclfvlb  37968  snhesn  37999  psshepw  38001
  Copyright terms: Public domain W3C validator