Theorem mprgbir 2588

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 2583	. 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 2200   A.wral 2508

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 1495

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

This theorem is referenced by:  ss2rabi  3307  rabnc  3525  ssintub  3944  tron  4477  djussxp  4873  dmiin  4976  dfco2  5234  coiun  5244  tfrlem6  6477  oacl  6623  sbthlem1  7147  peano1nnnn  8062  renfdisj  8229  1nn  9144  ioomax  10173  iccmax  10174  xnn0nnen  10689  fxnn0nninf  10691  fisumcom2  11989  fprodcom2fi  12177  bezoutlemmain  12559  dfphi2  12782  unennn  13008  znnen  13009  istopon  14727  neipsm  14868  lgsquadlem2  15797  pw0ss  15924  clwwlkn0  16203  bj-omtrans2  16488  nninfomnilem  16556  exmidsbthrlem  16562