Theorem mpgbir 1453

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

Step	Hyp	Ref	Expression
1		mpgbir.2	. . 3 |- ps
2	1	ax-gen 1449	. 2 |- A. x ps
3		mpgbir.1	. 2 |- ( ph <-> A. x ps )
4	2, 3	mpbir 146	1 |- ph

Syntax hints:   <-> wb 105   A.wal 1351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1449

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfi  1462  cvjust  2172  eqriv  2174  abbi2i  2292  nfci  2309  abid2f  2345  rgen  2530  ssriv  3161  ss2abi  3229  nel0  3446  ssmin  3865  intab  3875  iunab  3935  iinab  3950  sndisj  4001  disjxsn  4003  intid  4226  fr0  4353  zfregfr  4575  peano1  4595  relssi  4719  dm0  4843  dmi  4844  funopabeq  5254  isarep2  5305  fvopab3ig  5592  opabex  5742  acexmid  5876  finomni  7140  dfuzi  9365  fzodisj  10180  fzouzdisj  10182  bdelir  14638