Theorem mprgbir 2600

Description: Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)

Hypotheses

Ref	Expression
mprgbir.1	|- ( ph <-> A. x e. A ps )
mprgbir.2	|- ( x e. A -> ps )

Assertion

Ref	Expression
mprgbir	|- ph

Proof of Theorem mprgbir

Step	Hyp	Ref	Expression
1		mprgbir.2	. . 3 |- ( x e. A -> ps )
2	1	rgen 2595	. 2 |- A. x e. A ps
3		mprgbir.1	. 2 |- ( ph <-> A. x e. A ps )
4	2, 3	mpbir 146	1 |- ph

Syntax hints:   -> wi 4   <-> wb 105   e. wcel 2203   A.wral 2520

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 1498

This theorem depends on definitions:  df-bi 117  df-ral 2525

This theorem is referenced by:  ss2rabi  3320  rabnc  3541  ssintub  3967  tron  4503  djussxp  4900  dmiin  5003  dfco2  5262  coiun  5272  tfrlem6  6547  oacl  6693  sbthlem1  7227  peano1nnnn  8167  renfdisj  8333  1nn  9248  ioomax  10281  iccmax  10282  xnn0nnen  10799  fxnn0nninf  10801  fisumcom2  12124  fprodcom2fi  12312  bezoutlemmain  12694  dfphi2  12917  unennn  13148  znnen  13149  istopon  14878  neipsm  15019  lgsquadlem2  15951  pw0ss  16078  clwwlkn0  16403  bj-omtrans2  16727  nninfomnilem  16796  exmidsbthrlem  16802