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

Theorem sylnibr 677
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 132 . 2  |-  ( ps  <->  ch )
41, 3sylnib 676 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 105
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-in1 614  ax-in2 615
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  rexnalim  2466  nssr  3215  difdif  3260  unssin  3374  inssun  3375  undif3ss  3396  ssdif0im  3487  dcun  3533  prneimg  3772  iundif2ss  3949  nssssr  4219  pofun  4309  frirrg  4347  regexmidlem1  4529  dcdifsnid  6499  unfidisj  6915  fidcenumlemrks  6946  difinfsn  7093  pw1nel3  7224  addnqprlemfl  7546  addnqprlemfu  7547  mulnqprlemfl  7562  mulnqprlemfu  7563  cauappcvgprlemladdru  7643  caucvgprprlemaddq  7695  fzpreddisj  10054  fprodntrivap  11573  pw2dvdslemn  12145  isnsgrp  12701  ivthinclemdisj  13778  pwtrufal  14396  pw1nct  14401  nninfsellemsuc  14410
  Copyright terms: Public domain W3C validator