Theorem sylnib 331

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

Step	Hyp	Ref	Expression
1		sylnib.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		sylnib.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3	2	biimpri 231	. 2 ⊢ (𝜒 → 𝜓)
4	1, 3	nsyl 141	1 ⊢ (𝜑 → ¬ 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  sylnibr  332  neqcomd  2773  fr3nr  7772  omopthi  8648  cofonr  8661  inf3lem6  9603  rankxpsuc  9855  scotteld  9873  cflim2  10248  ssfin4  10295  fin23lem30  10327  isf32lem5  10342  gchhar  10665  qextlt  13230  qextle  13231  fzneuz  13638  vdwnn  17059  psgnunilem3  19567  efgredlemb  19817  gsumzsplit  19998  lspexchn2  21236  lspindp2l  21239  lspindp2  21240  psrlidm  22092  mplcoe1  22169  mplcoe5  22172  ptopn2  23722  regr1lem2  23878  rnelfmlem  24090  hauspwpwf1  24125  tsmssplit  24290  reconn  24967  itg2splitlem  25888  itg2split  25889  itg2cn  25903  wilthlem2  27211  bposlem9  27434  2sqcoprm  27577  elntg2  29313  nfrgr2v  30601  hatomistici  32692  nn0min  33143  ccatws1f1o  33249  esplyfvn  33945  fedgmullem2  33998  qqhf  34354  hasheuni  34453  oddpwdc  34722  ballotlemimin  34874  ballotlemfrcn0  34898  bnj1388  35399  prv1n  35901  efrunt  36183  dfon2lem4  36254  dfon2lem7  36257  nmulprop  36660  nandsym1  36911  atbase  40041  llnbase  40261  lplnbase  40286  lvolbase  40330  dalem48  40472  lhpbase  40750  cdlemg17pq  41424  cdlemg19  41436  cdlemg21  41438  dvh3dim3N  42201  fimgmcyc  43282  rmspecnonsq  43614  setindtr  43731  flcidc  43877  omssrncard  44246  fmul01lt1lem2  46281  icccncfext  46581  stoweidlem14  46708  stoweidlem26  46720  stirlinglem5  46772  fourierdlem42  46843  fourierdlem62  46862  fourierdlem66  46866  hoicvr  47242  chnsubseq  47576