Theorem sylnib 328

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 228	. 2 ⊢ (𝜒 → 𝜓)
4	1, 3	nsyl 140	1 ⊢ (𝜑 → ¬ 𝜒)

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

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 207

This theorem is referenced by:  sylnibr  329  neqcomd  2747  ssnelpss  4068  fr3nr  7727  omopthi  8599  cofonr  8612  inf3lem6  9554  rankxpsuc  9806  cflim2  10185  ssfin4  10232  fin23lem30  10264  isf32lem5  10279  gchhar  10602  qextlt  13130  qextle  13131  fzneuz  13536  vdwnn  16938  psgnunilem3  19437  efgredlemb  19687  gsumzsplit  19868  lspexchn2  21098  lspindp2l  21101  lspindp2  21102  psrlidm  21929  mplcoe1  22004  mplcoe5  22007  ptopn2  23540  regr1lem2  23696  rnelfmlem  23908  hauspwpwf1  23943  tsmssplit  24108  reconn  24785  itg2splitlem  25717  itg2split  25718  itg2cn  25732  wilthlem2  27047  bposlem9  27271  2sqcoprm  27414  elntg2  29070  nfrgr2v  30359  hatomistici  32449  nn0min  32911  ccatws1f1o  33043  esplyfvn  33753  fedgmullem2  33807  qqhf  34163  hasheuni  34262  oddpwdc  34531  ballotlemimin  34683  ballotlemfrcn0  34707  bnj1388  35208  prv1n  35644  efrunt  35926  dfon2lem4  35997  dfon2lem7  36000  nandsym1  36635  atbase  39659  llnbase  39879  lplnbase  39904  lvolbase  39948  dalem48  40090  lhpbase  40368  cdlemg17pq  41042  cdlemg19  41054  cdlemg21  41056  dvh3dim3N  41819  fimgmcyc  42898  rmspecnonsq  43258  setindtr  43375  flcidc  43521  omssrncard  43890  scotteld  44596  fmul01lt1lem2  45939  icccncfext  46239  stoweidlem14  46366  stoweidlem26  46378  stirlinglem5  46430  fourierdlem42  46501  fourierdlem62  46520  fourierdlem66  46524  hoicvr  46900  chnsubseq  47232