Theorem mprgbir 2608

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-ral 2533

This theorem is used by:  ss2rabi  3330  rabnc  3555  ssintub  3988  tron  4527  djussxp  4925  dmiin  5028  dfco2  5287  coiun  5297  tfrlem6  6587  oacl  6733  sbthlem1  7274  peano1nnnn  8219  renfdisj  8385  1nn  9315  ioomax  10350  iccmax  10351  xnn0nnen  10874  fxnn0nninf  10876  fisumcom2  12205  fprodcom2fi  12393  bezoutlemmain  12775  dfphi2  12998  unennn  13288  znnen  13289  istopon  15114  neipsm  15255  lgsquadlem2  16197  pw0ss  16324  clwwlkn0  16649  bj-omtrans2  16983  nninfomnilem  17061  exmidsbthrlem  17067