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

Theorem mpgbir 1453
Description: Modus ponens on biconditional combined with generalization. (Contributed by NM, 24-May-1994.) (Proof shortened by Stefan Allan, 28-Oct-2008.)
Hypotheses
Ref Expression
mpgbir.1 (𝜑 ↔ ∀𝑥𝜓)
mpgbir.2 𝜓
Assertion
Ref Expression
mpgbir 𝜑

Proof of Theorem mpgbir
StepHypRef Expression
1 mpgbir.2 . . 3 𝜓
21ax-gen 1449 . 2 𝑥𝜓
3 mpgbir.1 . 2 (𝜑 ↔ ∀𝑥𝜓)
42, 3mpbir 146 1 𝜑
Colors of variables: wff set class
Syntax hints:  wb 105  wal 1351
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
This theorem is referenced by:  nfi  1462  cvjust  2172  eqriv  2174  abbi2i  2292  nfci  2309  abid2f  2345  rgen  2530  ssriv  3159  ss2abi  3227  nel0  3444  ssmin  3861  intab  3871  iunab  3930  iinab  3945  sndisj  3996  disjxsn  3998  intid  4221  fr0  4348  zfregfr  4570  peano1  4590  relssi  4714  dm0  4837  dmi  4838  funopabeq  5248  isarep2  5299  fvopab3ig  5586  opabex  5736  acexmid  5868  finomni  7132  dfuzi  9349  fzodisj  10161  fzouzdisj  10163  bdelir  14248
  Copyright terms: Public domain W3C validator