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

Theorem mprgbir 2449
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 2444 . 2 𝑥𝐴 𝜓
3 mprgbir.1 . 2 (𝜑 ↔ ∀𝑥𝐴 𝜓)
42, 3mpbir 145 1 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wcel 1448  wral 2375
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1393
This theorem depends on definitions:  df-bi 116  df-ral 2380
This theorem is referenced by:  ss2rabi  3126  rabnc  3342  ssintub  3736  tron  4242  djussxp  4622  dmiin  4723  dfco2  4974  coiun  4984  tfrlem6  6143  oacl  6286  sbthlem1  6773  peano1nnnn  7539  renfdisj  7696  1nn  8589  ioomax  9572  iccmax  9573  fxnn0nninf  10052  fisumcom2  11046  bezoutlemmain  11479  dfphi2  11688  unennn  11702  znnen  11703  istopon  11962  neipsm  12105  bj-omtrans2  12740  nninfomnilem  12798  exmidsbthrlem  12801
  Copyright terms: Public domain W3C validator