Theorem mpgbir 1429

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 1425	. 2 |- A. x ps
3		mpgbir.1	. 2 |- ( ph <-> A. x ps )
4	2, 3	mpbir 145	1 |- ph

Syntax hints:   <-> wb 104   A.wal 1329

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nfi  1438  cvjust  2134  eqriv  2136  abbi2i  2254  nfci  2271  abid2f  2306  rgen  2485  ssriv  3101  ss2abi  3169  nel0  3384  ssmin  3790  intab  3800  iunab  3859  iinab  3874  sndisj  3925  disjxsn  3927  intid  4146  fr0  4273  zfregfr  4488  peano1  4508  relssi  4630  dm0  4753  dmi  4754  funopabeq  5159  isarep2  5210  fvopab3ig  5495  opabex  5644  acexmid  5773  finomni  7012  dfuzi  9161  fzodisj  9955  fzouzdisj  9957  bdelir  13045