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

Theorem sylnibr 635
Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting an consequent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)
Hypotheses
Ref Expression
sylnibr.1  |-  ( ph  ->  -.  ps )
sylnibr.2  |-  ( ch  <->  ps )
Assertion
Ref Expression
sylnibr  |-  ( ph  ->  -.  ch )

Proof of Theorem sylnibr
StepHypRef Expression
1 sylnibr.1 . 2  |-  ( ph  ->  -.  ps )
2 sylnibr.2 . . 3  |-  ( ch  <->  ps )
32bicomi 130 . 2  |-  ( ps  <->  ch )
41, 3sylnib 634 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  rexnalim  2360  nssr  3058  difdif  3098  unssin  3210  inssun  3211  undif3ss  3232  ssdif0im  3315  prneimg  3574  iundif2ss  3751  nssssr  3985  pofun  4075  frirrg  4113  regexmidlem1  4284  nndifsnid  6146  fidifsnid  6406  unfidisj  6442  addnqprlemfl  6811  addnqprlemfu  6812  mulnqprlemfl  6827  mulnqprlemfu  6828  cauappcvgprlemladdru  6908  caucvgprprlemaddq  6960  fzpreddisj  9164  pw2dvdslemn  10687
  Copyright terms: Public domain W3C validator