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  4041  disjxsn  4043  intid  4269  fr0  4399  zfregfr  4623  peano1  4643  relssi  4767  dm0  4893  dmi  4894  funopabeq  5308  isarep2  5362  fvopab3ig  5655  opabex  5810  acexmid  5945  finomni  7244  dfuzi  9485  fzodisj  10304  fzouzdisj  10306  bdelir  15820