Theorem mprgbir 2535

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 2530	. 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 2148   A.wral 2455

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 1449

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

This theorem is referenced by:  ss2rabi  3237  rabnc  3455  ssintub  3862  tron  4382  djussxp  4772  dmiin  4873  dfco2  5128  coiun  5138  tfrlem6  6316  oacl  6460  sbthlem1  6955  peano1nnnn  7850  renfdisj  8015  1nn  8928  ioomax  9946  iccmax  9947  fxnn0nninf  10435  fisumcom2  11441  fprodcom2fi  11629  bezoutlemmain  11993  dfphi2  12214  unennn  12392  znnen  12393  istopon  13444  neipsm  13585  bj-omtrans2  14629  nninfomnilem  14687  exmidsbthrlem  14690