Theorem mprgbir 2515

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

Syntax hints:   -> wi 4   <-> wb 104   e. wcel 2128   A.wral 2435

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

This theorem depends on definitions:  df-bi 116  df-ral 2440

This theorem is referenced by:  ss2rabi  3210  rabnc  3426  ssintub  3825  tron  4342  djussxp  4731  dmiin  4832  dfco2  5085  coiun  5095  tfrlem6  6263  oacl  6407  sbthlem1  6901  peano1nnnn  7772  renfdisj  7937  1nn  8844  ioomax  9852  iccmax  9853  fxnn0nninf  10337  fisumcom2  11335  fprodcom2fi  11523  bezoutlemmain  11882  dfphi2  12095  unennn  12137  znnen  12138  istopon  12422  neipsm  12565  bj-omtrans2  13543  nninfomnilem  13601  exmidsbthrlem  13604