Theorem mprgbir 2490

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 2485	. 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 1480   A.wral 2416

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 1425

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

This theorem is referenced by:  ss2rabi  3179  rabnc  3395  ssintub  3789  tron  4304  djussxp  4684  dmiin  4785  dfco2  5038  coiun  5048  tfrlem6  6213  oacl  6356  sbthlem1  6845  peano1nnnn  7660  renfdisj  7824  1nn  8731  ioomax  9731  iccmax  9732  fxnn0nninf  10211  fisumcom2  11207  bezoutlemmain  11686  dfphi2  11896  unennn  11910  znnen  11911  istopon  12180  neipsm  12323  bj-omtrans2  13155  nninfomnilem  13214  exmidsbthrlem  13217