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

Theorem mprgbir 2535
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 2530 . 2  |-  A. x  e.  A  ps
3 mprgbir.1 . 2  |-  ( ph  <->  A. x  e.  A  ps )
42, 3mpbir 146 1  |-  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105    e. wcel 2148   A.wral 2455
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 1449
This theorem depends on definitions:  df-bi 117  df-ral 2460
This theorem is referenced by:  ss2rabi  3237  rabnc  3455  ssintub  3862  tron  4382  djussxp  4772  dmiin  4873  dfco2  5128  coiun  5138  tfrlem6  6316  oacl  6460  sbthlem1  6955  peano1nnnn  7850  renfdisj  8015  1nn  8928  ioomax  9946  iccmax  9947  fxnn0nninf  10435  fisumcom2  11441  fprodcom2fi  11629  bezoutlemmain  11993  dfphi2  12214  unennn  12392  znnen  12393  istopon  13444  neipsm  13585  bj-omtrans2  14629  nninfomnilem  14687  exmidsbthrlem  14690
  Copyright terms: Public domain W3C validator