Theorem mprgbir 2591

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 2586	. 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 2202   A.wral 2511

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 1498

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

This theorem is referenced by:  ss2rabi  3310  rabnc  3529  ssintub  3951  tron  4485  djussxp  4881  dmiin  4984  dfco2  5243  coiun  5253  tfrlem6  6525  oacl  6671  sbthlem1  7199  peano1nnnn  8132  renfdisj  8298  1nn  9213  ioomax  10244  iccmax  10245  xnn0nnen  10762  fxnn0nninf  10764  fisumcom2  12079  fprodcom2fi  12267  bezoutlemmain  12649  dfphi2  12872  unennn  13098  znnen  13099  istopon  14824  neipsm  14965  lgsquadlem2  15897  pw0ss  16024  clwwlkn0  16349  bj-omtrans2  16673  nninfomnilem  16744  exmidsbthrlem  16750