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

Theorem mpgbir 1560
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 1556 . 2  |-  A. x ps
3 mpgbir.1 . 2  |-  ( ph  <->  A. x ps )
42, 3mpbir 202 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 178   A.wal 1550
This theorem is referenced by:  nfi  1561  cvjust  2433  eqriv  2435  abbi2i  2549  nfci  2564  abid2f  2599  rgen  2773  ssriv  3354  ss2abi  3417  ssmin  4071  intab  4082  iunab  4139  iinab  4154  sndisj  4206  disjxsn  4208  intid  4423  fr0  4563  onfr  4622  ordom  4856  relssi  4969  dm0  5085  dmi  5086  funopabeq  5489  isarep2  5535  fvopab3ig  5805  opabex  5966  caovmo  6286  opabiotafun  6538  tz7.44lem1  6665  dfsup2  7449  dfsup2OLD  7450  zfregfr  7572  dfom3  7604  trcl  7666  tc2  7683  rankf  7722  rankval4  7795  uniwun  8617  dfnn2  10015  dfuzi  10362  fzodisj  11169  fzouzdisj  11171  cycsubg  14970  efger  15352  ajfuni  22363  funadj  23391  rabexgfGS  23989  abrexdomjm  23990  ballotth  24797  dfon3  25739  fnsingle  25766  dfiota3  25770  hftr  26125  ismblfin  26249  abrexdom  26434  compab  27622  dvcosre  27719  stoweidlem44  27771  onfrALT  28697  bnj1133  29420
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator