MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylnib Structured version   Visualization version   GIF version

Theorem sylnib 329
Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.)
Hypotheses
Ref Expression
sylnib.1 (𝜑 → ¬ 𝜓)
sylnib.2 (𝜓𝜒)
Assertion
Ref Expression
sylnib (𝜑 → ¬ 𝜒)

Proof of Theorem sylnib
StepHypRef Expression
1 sylnib.1 . 2 (𝜑 → ¬ 𝜓)
2 sylnib.2 . . 3 (𝜓𝜒)
32biimpri 229 . 2 (𝜒𝜓)
41, 3nsyl 142 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 208
This theorem is referenced by:  sylnibr  330  neqcomd  2828  ssnelpss  4085  fr3nr  7483  omopthi  8273  inf3lem6  9084  rankxpsuc  9299  cflim2  9673  ssfin4  9720  fin23lem30  9752  isf32lem5  9767  gchhar  10089  qextlt  12584  qextle  12585  fzneuz  12976  vdwnn  16322  psgnunilem3  18553  efgredlemb  18801  gsumzsplit  18976  lspexchn2  19832  lspindp2l  19835  lspindp2  19836  psrlidm  20111  mplcoe1  20174  mplcoe5  20177  ptopn2  22120  regr1lem2  22276  rnelfmlem  22488  hauspwpwf1  22523  tsmssplit  22687  reconn  23363  itg2splitlem  24276  itg2split  24277  itg2cn  24291  wilthlem2  25573  bposlem9  25795  2sqcoprm  25938  elntg2  26698  nfrgr2v  27978  hatomistici  30066  nn0min  30463  fedgmullem2  30925  qqhf  31126  hasheuni  31243  oddpwdc  31511  ballotlemimin  31662  ballotlemfrcn0  31686  bnj1388  32202  prv1n  32575  efrunt  32836  dfon2lem4  32928  dfon2lem7  32931  nandsym1  33667  atbase  36305  llnbase  36525  lplnbase  36550  lvolbase  36594  dalem48  36736  lhpbase  37014  cdlemg17pq  37688  cdlemg19  37700  cdlemg21  37702  dvh3dim3N  38465  rmspecnonsq  39382  setindtr  39499  flcidc  39652  scotteld  40459  fmul01lt1lem2  41742  icccncfext  42046  stoweidlem14  42176  stoweidlem26  42188  stirlinglem5  42240  fourierdlem42  42311  fourierdlem62  42330  fourierdlem66  42334  hoicvr  42707
  Copyright terms: Public domain W3C validator