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

Theorem mprgbir 2422
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 2417 . 2  |-  A. x  e.  A  ps
3 mprgbir.1 . 2  |-  ( ph  <->  A. x  e.  A  ps )
42, 3mpbir 144 1  |-  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    e. wcel 1434   A.wral 2349
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1379
This theorem depends on definitions:  df-bi 115  df-ral 2354
This theorem is referenced by:  ss2rabi  3077  rabnc  3284  ssintub  3662  tron  4145  djussxp  4509  dmiin  4608  dfco2  4850  coiun  4860  tfrlem6  5965  oacl  6104  peano1nnnn  7082  renfdisj  7239  1nn  8117  ioomax  9047  iccmax  9048  bezoutlemmain  10531  unennn  10735  znnen  10736  bj-omtrans2  10937
  Copyright terms: Public domain W3C validator