Theorem mprgbir 2493

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 2488	. 2 |- A. x e. A ps
3		mprgbir.1	. 2 |- ( ph <-> A. x e. A ps )
4	2, 3	mpbir 145	1 |- ph

Syntax hints:   -> wi 4   <-> wb 104   e. wcel 1481   A.wral 2417

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

This theorem depends on definitions:  df-bi 116  df-ral 2422

This theorem is referenced by:  ss2rabi  3184  rabnc  3400  ssintub  3797  tron  4312  djussxp  4692  dmiin  4793  dfco2  5046  coiun  5056  tfrlem6  6221  oacl  6364  sbthlem1  6853  peano1nnnn  7684  renfdisj  7848  1nn  8755  ioomax  9761  iccmax  9762  fxnn0nninf  10242  fisumcom2  11239  bezoutlemmain  11722  dfphi2  11932  unennn  11946  znnen  11947  istopon  12219  neipsm  12362  bj-omtrans2  13326  nninfomnilem  13389  exmidsbthrlem  13392