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

Theorem mpgbir 1537
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 1533 . 2  |-  A. x ps
3 mpgbir.1 . 2  |-  ( ph  <->  A. x ps )
42, 3mpbir 200 1  |-  ph
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1527
This theorem is referenced by:  nfi  1538  cvjust  2278  eqriv  2280  abbi2i  2394  nfci  2409  abid2f  2444  rgen  2608  ssriv  3184  ss2abi  3245  ssmin  3881  intab  3892  iunab  3948  iinab  3963  sndisj  4015  disjxsn  4017  intid  4231  fr0  4372  onfr  4431  ordom  4665  relssi  4778  dm0  4892  dmi  4893  funopabeq  5288  isarep2  5332  fvopab3ig  5599  opabex  5744  caovmo  6057  opabiotafun  6291  tz7.44lem1  6418  dfsup2  7195  dfsup2OLD  7196  zfregfr  7316  dfom3  7348  trcl  7410  tc2  7427  rankf  7466  rankval4  7539  uniwun  8362  dfnn2  9759  dfuzi  10102  fzodisj  10900  fzouzdisj  10902  cycsubg  14645  efger  15027  ajfuni  21438  funadj  22466  abrexdomjm  23165  dfon3  24432  fnsingle  24458  dfiota3  24462  hftr  24812  eqriv2  24947  eqint  24960  inpc  25277  dominc  25280  rninc  25281  pgapspf  26052  abrexdom  26405  compab  27644  onfrALT  28314  bnj1133  29019
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator