Theorem mprgbir 2564

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 2559	. 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 2176   A.wral 2484

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 1472

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

This theorem is referenced by:  ss2rabi  3275  rabnc  3493  ssintub  3903  tron  4430  djussxp  4824  dmiin  4925  dfco2  5183  coiun  5193  tfrlem6  6404  oacl  6548  sbthlem1  7061  peano1nnnn  7967  renfdisj  8134  1nn  9049  ioomax  10072  iccmax  10073  xnn0nnen  10584  fxnn0nninf  10586  fisumcom2  11782  fprodcom2fi  11970  bezoutlemmain  12352  dfphi2  12575  unennn  12801  znnen  12802  istopon  14518  neipsm  14659  lgsquadlem2  15588  bj-omtrans2  15930  nninfomnilem  15992  exmidsbthrlem  15998