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

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

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  2750  fr3nr  7722  omopthi  8594  cofonr  8607  inf3lem6  9552  rankxpsuc  9804  cflim2  10183  ssfin4  10230  fin23lem30  10262  isf32lem5  10277  gchhar  10600  qextlt  13153  qextle  13154  fzneuz  13560  vdwnn  16967  psgnunilem3  19469  efgredlemb  19719  gsumzsplit  19900  lspexchn2  21131  lspindp2l  21134  lspindp2  21135  psrlidm  21943  mplcoe1  22020  mplcoe5  22023  ptopn2  23574  regr1lem2  23730  rnelfmlem  23942  hauspwpwf1  23977  tsmssplit  24142  reconn  24819  itg2splitlem  25740  itg2split  25741  itg2cn  25755  wilthlem2  27057  bposlem9  27280  2sqcoprm  27423  elntg2  29079  nfrgr2v  30367  hatomistici  32458  nn0min  32920  ccatws1f1o  33037  esplyfvn  33768  fedgmullem2  33821  qqhf  34177  hasheuni  34276  oddpwdc  34545  ballotlemimin  34697  ballotlemfrcn0  34721  bnj1388  35222  prv1n  35666  efrunt  35948  dfon2lem4  36019  dfon2lem7  36022  nandsym1  36657  atbase  39788  llnbase  40008  lplnbase  40033  lvolbase  40077  dalem48  40219  lhpbase  40497  cdlemg17pq  41171  cdlemg19  41183  cdlemg21  41185  dvh3dim3N  41948  fimgmcyc  43027  rmspecnonsq  43359  setindtr  43476  flcidc  43622  omssrncard  43991  scotteld  44697  fmul01lt1lem2  46037  icccncfext  46337  stoweidlem14  46464  stoweidlem26  46476  stirlinglem5  46528  fourierdlem42  46599  fourierdlem62  46618  fourierdlem66  46622  hoicvr  46998  chnsubseq  47332