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

Theorem mpgbir 1595
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 1591 . 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 1367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  nfi  1596  cvjust  2438  eqriv  2440  abbi2i  2559  nfci  2574  abid2f  2609  rgen  2786  ssriv  3365  ss2abi  3429  ssmin  4152  intab  4163  iunab  4221  iinab  4236  sndisj  4289  disjxsn  4291  intid  4555  fr0  4704  onfr  4763  relssi  4936  dm0  5058  dmi  5059  funopabeq  5457  isarep2  5503  opabiotafun  5757  fvopab3ig  5776  opabex  5951  caovmo  6305  ordom  6490  tz7.44lem1  6866  dfsup2  7697  dfsup2OLD  7698  zfregfr  7823  dfom3  7858  trcl  7953  tc2  7967  rankf  8006  rankval4  8079  uniwun  8912  dfnn2  10340  dfuzi  10737  fzodisj  11588  fzouzdisj  11590  cycsubg  15714  efger  16220  ajfuni  24265  funadj  25295  rabexgfGS  25891  abrexdomjm  25893  ballotth  26925  dfon3  27928  fnsingle  27955  dfiota3  27959  hftr  28225  ismblfin  28437  abrexdom  28629  compab  29702  dvcosre  29793  stoweidlem44  29844  alimp-surprise  31137  onfrALT  31262  bnj1133  31985  bj-abbi2i  32302  bj-rabtrALT  32438  bj-nel0  32444
  Copyright terms: Public domain W3C validator