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

Theorem sylnibr 643
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 131 . 2 (𝜓𝜒)
41, 3sylnib 642 1 (𝜑 → ¬ 𝜒)
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 584  ax-in2 585
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  rexnalim  2386  nssr  3107  difdif  3148  unssin  3262  inssun  3263  undif3ss  3284  ssdif0im  3374  dcun  3420  prneimg  3648  iundif2ss  3825  nssssr  4082  pofun  4172  frirrg  4210  regexmidlem1  4386  dcdifsnid  6330  unfidisj  6739  fidcenumlemrks  6769  difinfsn  6900  addnqprlemfl  7268  addnqprlemfu  7269  mulnqprlemfl  7284  mulnqprlemfu  7285  cauappcvgprlemladdru  7365  caucvgprprlemaddq  7417  fzpreddisj  9692  pw2dvdslemn  11635  pwtrufal  12777  nninfsellemsuc  12792
  Copyright terms: Public domain W3C validator