Theorem mpgbir 1383

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

Syntax hints:   <-> wb 103   A.wal 1283

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  nfi  1392  cvjust  2077  eqriv  2079  abbi2i  2194  nfci  2210  abid2f  2244  rgen  2417  ssriv  3004  ss2abi  3067  ssmin  3663  intab  3673  iunab  3732  iinab  3747  sndisj  3789  disjxsn  3791  intid  3987  fr0  4114  zfregfr  4324  peano1  4343  relssi  4457  dm0  4577  dmi  4578  funopabeq  4966  isarep2  5017  fvopab3ig  5278  opabex  5417  acexmid  5542  dfuzi  8538  fzodisj  9264  fzouzdisj  9266  bdelir  10796