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

Theorem mpgbir 1556
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 1552 . 2  |-  A. x ps
3 mpgbir.1 . 2  |-  ( ph  <->  A. x ps )
42, 3mpbir 201 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1546
This theorem is referenced by:  nfi  1557  cvjust  2399  eqriv  2401  abbi2i  2515  nfci  2530  abid2f  2565  rgen  2731  ssriv  3312  ss2abi  3375  ssmin  4029  intab  4040  iunab  4097  iinab  4112  sndisj  4164  disjxsn  4166  intid  4381  fr0  4521  onfr  4580  ordom  4813  relssi  4926  dm0  5042  dmi  5043  funopabeq  5446  isarep2  5492  fvopab3ig  5762  opabex  5923  caovmo  6243  opabiotafun  6495  tz7.44lem1  6622  dfsup2  7405  dfsup2OLD  7406  zfregfr  7526  dfom3  7558  trcl  7620  tc2  7637  rankf  7676  rankval4  7749  uniwun  8571  dfnn2  9969  dfuzi  10316  fzodisj  11122  fzouzdisj  11124  cycsubg  14923  efger  15305  ajfuni  22314  funadj  23342  rabexgfGS  23940  abrexdomjm  23941  ballotth  24748  dfon3  25646  fnsingle  25672  dfiota3  25676  hftr  26027  ismblfin  26146  abrexdom  26322  compab  27511  dvcosre  27608  stoweidlem44  27660  onfrALT  28346  bnj1133  29064
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator