ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mprgbir Unicode version

Theorem mprgbir 2465
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
StepHypRef Expression
1 mprgbir.2 . . 3  |-  ( x  e.  A  ->  ps )
21rgen 2460 . 2  |-  A. x  e.  A  ps
3 mprgbir.1 . 2  |-  ( ph  <->  A. x  e.  A  ps )
42, 3mpbir 145 1  |-  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    e. wcel 1463   A.wral 2391
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 1408
This theorem depends on definitions:  df-bi 116  df-ral 2396
This theorem is referenced by:  ss2rabi  3147  rabnc  3363  ssintub  3757  tron  4272  djussxp  4652  dmiin  4753  dfco2  5006  coiun  5016  tfrlem6  6179  oacl  6322  sbthlem1  6811  peano1nnnn  7624  renfdisj  7788  1nn  8691  ioomax  9682  iccmax  9683  fxnn0nninf  10162  fisumcom2  11158  bezoutlemmain  11593  dfphi2  11802  unennn  11816  znnen  11817  istopon  12086  neipsm  12229  bj-omtrans2  12989  nninfomnilem  13048  exmidsbthrlem  13051
  Copyright terms: Public domain W3C validator