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

Theorem sylnibr 666
 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 665 1 (𝜑 → ¬ 𝜒)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  rexnalim  2427  nssr  3157  difdif  3201  unssin  3315  inssun  3316  undif3ss  3337  ssdif0im  3427  dcun  3473  prneimg  3701  iundif2ss  3878  nssssr  4144  pofun  4234  frirrg  4272  regexmidlem1  4448  dcdifsnid  6400  unfidisj  6810  fidcenumlemrks  6841  difinfsn  6985  addnqprlemfl  7379  addnqprlemfu  7380  mulnqprlemfl  7395  mulnqprlemfu  7396  cauappcvgprlemladdru  7476  caucvgprprlemaddq  7528  fzpreddisj  9863  pw2dvdslemn  11854  ivthinclemdisj  12801  pwtrufal  13251  pw1nct  13257  nninfsellemsuc  13269
 Copyright terms: Public domain W3C validator