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

Theorem sylnib 648
Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.)
Hypotheses
Ref Expression
sylnib.1  |-  ( ph  ->  -.  ps )
sylnib.2  |-  ( ps  <->  ch )
Assertion
Ref Expression
sylnib  |-  ( ph  ->  -.  ch )

Proof of Theorem sylnib
StepHypRef Expression
1 sylnib.1 . 2  |-  ( ph  ->  -.  ps )
2 sylnib.2 . . 3  |-  ( ps  <->  ch )
32a1i 9 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
41, 3mtbid 644 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:  sylnibr  649  inssdif0im  3396  undifexmid  4077  ordtriexmidlem2  4396  dmsn0el  4966  fidifsnen  6717  ctssdccl  6948  ltpopr  7351  caucvgprprlemnbj  7449  xrlttri3  9476  fzneuz  9774  iseqf1olemqcl  10152  iseqf1olemnab  10154  iseqf1olemab  10155  exp3val  10188  pwle2  12885
  Copyright terms: Public domain W3C validator