Theorem mprgbir 2422

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 2417	. 2 |- A. x e. A ps
3		mprgbir.1	. 2 |- ( ph <-> A. x e. A ps )
4	2, 3	mpbir 144	1 |- ph

Syntax hints:   -> wi 4   <-> wb 103   e. wcel 1434   A.wral 2349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1379

This theorem depends on definitions:  df-bi 115  df-ral 2354

This theorem is referenced by:  ss2rabi  3077  rabnc  3284  ssintub  3662  tron  4145  djussxp  4509  dmiin  4608  dfco2  4850  coiun  4860  tfrlem6  5965  oacl  6104  peano1nnnn  7082  renfdisj  7239  1nn  8117  ioomax  9047  iccmax  9048  bezoutlemmain  10531  unennn  10735  znnen  10736  bj-omtrans2  10937