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

Theorem sylnibr 612
 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 127 . 2 (𝜓𝜒)
41, 3sylnib 611 1 (𝜑 → ¬ 𝜒)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  rexnalim  2334  nssr  3031  difdif  3097  unssin  3204  inssun  3205  undif3ss  3226  ssdif0im  3314  prneimg  3573  iundif2ss  3750  nssssr  3986  pofun  4077  frirrg  4115  regexmidlem1  4286  nndifsnid  6111  fidifsnid  6363  addnqprlemfl  6715  addnqprlemfu  6716  mulnqprlemfl  6731  mulnqprlemfu  6732  cauappcvgprlemladdru  6812  caucvgprprlemaddq  6864  fzpreddisj  9035  pw2dvdslemn  10253
 Copyright terms: Public domain W3C validator