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

Theorem mprgbir 2396
Description: Modus ponens on biconditional combined with restricted generalization. (Contributed by NM, 21-Mar-2004.)
Hypotheses
Ref Expression
mprgbir.1 (𝜑 ↔ ∀𝑥𝐴 𝜓)
mprgbir.2 (𝑥𝐴𝜓)
Assertion
Ref Expression
mprgbir 𝜑

Proof of Theorem mprgbir
StepHypRef Expression
1 mprgbir.2 . . 3 (𝑥𝐴𝜓)
21rgen 2391 . 2 𝑥𝐴 𝜓
3 mprgbir.1 . 2 (𝜑 ↔ ∀𝑥𝐴 𝜓)
42, 3mpbir 138 1 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102  wcel 1409  wral 2323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354
This theorem depends on definitions:  df-bi 114  df-ral 2328
This theorem is referenced by:  ss2rabi  3050  rabnc  3278  ssintub  3661  tron  4147  djussxp  4509  dmiin  4608  dfco2  4848  coiun  4858  tfrlem6  5963  oacl  6071  peano1nnnn  6986  renfdisj  7138  1nn  8001  ioomax  8918  iccmax  8919  bj-omtrans2  10469
  Copyright terms: Public domain W3C validator