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

Theorem mprgbir 2494
 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 2489 . 2 𝑥𝐴 𝜓
3 mprgbir.1 . 2 (𝜑 ↔ ∀𝑥𝐴 𝜓)
42, 3mpbir 145 1 𝜑
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104   ∈ wcel 1481  ∀wral 2417 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 1426 This theorem depends on definitions:  df-bi 116  df-ral 2422 This theorem is referenced by:  ss2rabi  3185  rabnc  3401  ssintub  3798  tron  4313  djussxp  4693  dmiin  4794  dfco2  5047  coiun  5057  tfrlem6  6222  oacl  6365  sbthlem1  6855  peano1nnnn  7704  renfdisj  7868  1nn  8775  ioomax  9781  iccmax  9782  fxnn0nninf  10262  fisumcom2  11259  bezoutlemmain  11742  dfphi2  11952  unennn  11966  znnen  11967  istopon  12239  neipsm  12382  bj-omtrans2  13346  nninfomnilem  13408  exmidsbthrlem  13411
 Copyright terms: Public domain W3C validator