Theorem mpgbir 1477

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 1473	. 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 1371

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 1473

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfi  1486  cvjust  2202  eqriv  2204  abbi2i  2322  nfci  2340  abid2f  2376  rgen  2561  ssriv  3205  ss2abi  3273  nel0  3490  ssmin  3918  intab  3928  iunab  3988  iinab  4003  sndisj  4055  disjxsn  4057  intid  4286  fr0  4416  zfregfr  4640  peano1  4660  relssi  4784  dm0  4911  dmi  4912  funopabeq  5326  isarep2  5380  fvopab3ig  5676  opabex  5831  acexmid  5966  finomni  7268  dfuzi  9518  fzodisj  10337  fzouzdisj  10339  fzodisjsn  10341  bdelir  15982