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  6482  oacl  6628  sbthlem1  7156  peano1nnnn  8072  renfdisj  8239  1nn  9154  ioomax  10183  iccmax  10184  xnn0nnen  10700  fxnn0nninf  10702  fisumcom2  12017  fprodcom2fi  12205  bezoutlemmain  12587  dfphi2  12810  unennn  13036  znnen  13037  istopon  14756  neipsm  14897  lgsquadlem2  15826  pw0ss  15953  clwwlkn0  16278  bj-omtrans2  16603  nninfomnilem  16671  exmidsbthrlem  16677