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

Theorem mprgbir 2548
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 2543 . 2 𝑥𝐴 𝜓
3 mprgbir.1 . 2 (𝜑 ↔ ∀𝑥𝐴 𝜓)
42, 3mpbir 146 1 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wcel 2160  wral 2468
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 1460
This theorem depends on definitions:  df-bi 117  df-ral 2473
This theorem is referenced by:  ss2rabi  3252  rabnc  3470  ssintub  3877  tron  4400  djussxp  4790  dmiin  4891  dfco2  5146  coiun  5156  tfrlem6  6340  oacl  6484  sbthlem1  6985  peano1nnnn  7880  renfdisj  8046  1nn  8959  ioomax  9977  iccmax  9978  fxnn0nninf  10468  fisumcom2  11477  fprodcom2fi  11665  bezoutlemmain  12030  dfphi2  12251  unennn  12447  znnen  12448  istopon  13965  neipsm  14106  bj-omtrans2  15162  nninfomnilem  15221  exmidsbthrlem  15224
  Copyright terms: Public domain W3C validator