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

Theorem sylnibr 602
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 601 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  2317  nssr  3003  difdif  3069  unssin  3176  inssun  3177  undif3ss  3198  ssdif0im  3286  prneimg  3545  iundif2ss  3722  nssssr  3958  pofun  4049  frirrg  4087  regexmidlem1  4258  nndifsnid  6080  fidifsnid  6332  addnqprlemfl  6655  addnqprlemfu  6656  mulnqprlemfl  6671  mulnqprlemfu  6672  cauappcvgprlemladdru  6752  caucvgprprlemaddq  6804  fzpreddisj  8931
  Copyright terms: Public domain W3C validator