Theorem mpgbir 1433

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 1429	. 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 1333

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 1429

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  nfi  1442  cvjust  2152  eqriv  2154  abbi2i  2272  nfci  2289  abid2f  2325  rgen  2510  ssriv  3132  ss2abi  3200  nel0  3415  ssmin  3826  intab  3836  iunab  3895  iinab  3910  sndisj  3961  disjxsn  3963  intid  4184  fr0  4311  zfregfr  4533  peano1  4553  relssi  4677  dm0  4800  dmi  4801  funopabeq  5206  isarep2  5257  fvopab3ig  5542  opabex  5691  acexmid  5823  finomni  7083  dfuzi  9274  fzodisj  10077  fzouzdisj  10079  bdelir  13422