Theorem mpgbir 1476

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 1472	. 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 1472

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nfi  1485  cvjust  2200  eqriv  2202  abbi2i  2320  nfci  2338  abid2f  2374  rgen  2559  ssriv  3197  ss2abi  3265  nel0  3482  ssmin  3904  intab  3914  iunab  3974  iinab  3989  sndisj  4040  disjxsn  4042  intid  4268  fr0  4398  zfregfr  4622  peano1  4642  relssi  4766  dm0  4892  dmi  4893  funopabeq  5307  isarep2  5361  fvopab3ig  5653  opabex  5808  acexmid  5943  finomni  7242  dfuzi  9483  fzodisj  10302  fzouzdisj  10304  bdelir  15783