Theorem mprgbir 2590

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 2585	. 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 2202   A.wral 2510

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 1497

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

This theorem is referenced by:  ss2rabi  3309  rabnc  3527  ssintub  3946  tron  4479  djussxp  4875  dmiin  4978  dfco2  5236  coiun  5246  tfrlem6  6481  oacl  6627  sbthlem1  7155  peano1nnnn  8071  renfdisj  8238  1nn  9153  ioomax  10182  iccmax  10183  xnn0nnen  10698  fxnn0nninf  10700  fisumcom2  11998  fprodcom2fi  12186  bezoutlemmain  12568  dfphi2  12791  unennn  13017  znnen  13018  istopon  14736  neipsm  14877  lgsquadlem2  15806  pw0ss  15933  clwwlkn0  16258  bj-omtrans2  16552  nninfomnilem  16620  exmidsbthrlem  16626