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

Theorem sylnibr 635
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 130 . 2 (𝜓𝜒)
41, 3sylnib 634 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  rexnalim  2366  nssr  3073  difdif  3114  unssin  3227  inssun  3228  undif3ss  3249  ssdif0im  3335  prneimg  3601  iundif2ss  3778  nssssr  4023  pofun  4113  frirrg  4151  regexmidlem1  4322  dcdifsnid  6217  unfidisj  6584  addnqprlemfl  7062  addnqprlemfu  7063  mulnqprlemfl  7078  mulnqprlemfu  7079  cauappcvgprlemladdru  7159  caucvgprprlemaddq  7211  fzpreddisj  9415  pw2dvdslemn  11025  nninfsellemsuc  11349
  Copyright terms: Public domain W3C validator