Theorem mprgbir 2421

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 2416	. 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 1433   A.wral 2348

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 1378

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

This theorem is referenced by:  ss2rabi  3076  rabnc  3277  ssintub  3654  tron  4137  djussxp  4499  dmiin  4598  dfco2  4840  coiun  4850  tfrlem6  5955  oacl  6063  peano1nnnn  7020  renfdisj  7172  1nn  8050  ioomax  8971  iccmax  8972  bezoutlemmain  10387  bj-omtrans2  10752