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

Theorem mpgbir 1318
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 (φxψ)
mpgbir.2 ψ
Assertion
Ref Expression
mpgbir φ

Proof of Theorem mpgbir
StepHypRef Expression
1 mpgbir.2 . . 3 ψ
21ax-gen 1314 . 2 xψ
3 mpgbir.1 . 2 (φxψ)
42, 3mpbir 134 1 φ
Colors of variables: wff set class
Syntax hints:  wb 98  wal 1224
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1314
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  nfi  1327  cvjust  2013  eqriv  2015  abbi2i  2130  nfci  2146  abid2f  2180  rgen  2348  ssriv  2922  ss2abi  2985  ssmin  3604  intab  3614  iunab  3673  iinab  3688  sndisj  3730  disjxsn  3732  intid  3930  peano1  4240  relssi  4354  dm0  4472  dmi  4473  funopabeq  4858  isarep2  4908  fvopab3ig  5167  opabex  5306  acexmid  5431  bdelir  7213
  Copyright terms: Public domain W3C validator