Theorem mpgbir 1726

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

Syntax hints:   <-> wb 196   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  nfiOLD  1734  cvjust  2617  eqriv  2619  abbi2i  2738  nfci  2754  abid2f  2791  rgen  2922  ssriv  3607  ss2abi  3674  nel0  3932  rab0  3955  abf  3978  ssmin  4496  intab  4507  iunab  4566  iinab  4581  sndisj  4644  disjxsn  4646  intid  4926  fr0  5093  relssi  5211  dmi  5340  onfr  5763  funopabeq  5924  isarep2  5978  opabiotafun  6259  fvopab3ig  6278  opabex  6483  caovmo  6871  ordom  7074  tz7.44lem1  7501  dfsup2  8350  zfregfr  8509  dfom3  8544  trcl  8604  tc2  8618  rankf  8657  rankval4  8730  uniwun  9562  dfnn2  11033  dfuzi  11468  fzodisj  12502  fzodisjsn  12505  cycsubg  17622  efger  18131  ajfuni  27715  funadj  28745  rabexgfGS  29340  abrexdomjm  29345  ballotth  30599  bnj1133  31057  dfon3  31999  fnsingle  32026  dfiota3  32030  hftr  32289  bj-abbi2i  32776  bj-rabtrALT  32927  bj-df-v  33016  ismblfin  33450  abrexdom  33525  cllem0  37871  cotrintab  37921  brtrclfv2  38019  snhesn  38080  psshepw  38082  k0004val0  38452  compab  38645  onfrALT  38764  dvcosre  40126  alimp-surprise  42526