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  3238  rabnc  3456  ssintub  3863  tron  4383  djussxp  4773  dmiin  4874  dfco2  5129  coiun  5139  tfrlem6  6317  oacl  6461  sbthlem1  6956  peano1nnnn  7851  renfdisj  8017  1nn  8930  ioomax  9948  iccmax  9949  fxnn0nninf  10438  fisumcom2  11446  fprodcom2fi  11634  bezoutlemmain  11999  dfphi2  12220  unennn  12398  znnen  12399  istopon  13516  neipsm  13657  bj-omtrans2  14712  nninfomnilem  14770  exmidsbthrlem  14773