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

Theorem sylnibr 649
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 131 . 2  |-  ( ps  <->  ch )
41, 3sylnib 648 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 104
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-in1 586  ax-in2 587
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  rexnalim  2401  nssr  3123  difdif  3167  unssin  3281  inssun  3282  undif3ss  3303  ssdif0im  3393  dcun  3439  prneimg  3667  iundif2ss  3844  nssssr  4104  pofun  4194  frirrg  4232  regexmidlem1  4408  dcdifsnid  6354  unfidisj  6763  fidcenumlemrks  6793  difinfsn  6937  addnqprlemfl  7315  addnqprlemfu  7316  mulnqprlemfl  7331  mulnqprlemfu  7332  cauappcvgprlemladdru  7412  caucvgprprlemaddq  7464  fzpreddisj  9744  pw2dvdslemn  11688  pwtrufal  12884  nninfsellemsuc  12900
  Copyright terms: Public domain W3C validator