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

Theorem sylnibr 601
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 (φ → ¬ ψ)
sylnibr.2 (χψ)
Assertion
Ref Expression
sylnibr (φ → ¬ χ)

Proof of Theorem sylnibr
StepHypRef Expression
1 sylnibr.1 . 2 (φ → ¬ ψ)
2 sylnibr.2 . . 3 (χψ)
32bicomi 123 . 2 (ψχ)
41, 3sylnib 600 1 (φ → ¬ χ)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 98
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-in1 544  ax-in2 545
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  rexnalim  2311  nssr  2997  difdif  3063  unssin  3170  inssun  3171  undif3ss  3192  ssdif0im  3280  prneimg  3536  iundif2ss  3713  nssssr  3949  pofun  4040  regexmidlem1  4218  addnqprlemfl  6539  addnqprlemfu  6540  cauappcvgprlemladdru  6627  fzpreddisj  8683
  Copyright terms: Public domain W3C validator