Theorem sylnib 330

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

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

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 209

This theorem is referenced by:  sylnibr  331  neqcomd  2771  fr3nr  7751  omopthi  8626  cofonr  8639  inf3lem6  9585  rankxpsuc  9837  cflim2  10217  ssfin4  10264  fin23lem30  10296  isf32lem5  10311  gchhar  10634  qextlt  13203  qextle  13204  fzneuz  13610  vdwnn  17017  psgnunilem3  19519  efgredlemb  19769  gsumzsplit  19950  lspexchn2  21181  lspindp2l  21184  lspindp2  21185  psrlidm  21993  mplcoe1  22070  mplcoe5  22073  ptopn2  23624  regr1lem2  23780  rnelfmlem  23992  hauspwpwf1  24027  tsmssplit  24192  reconn  24869  itg2splitlem  25790  itg2split  25791  itg2cn  25805  wilthlem2  27110  bposlem9  27333  2sqcoprm  27476  elntg2  29132  nfrgr2v  30420  hatomistici  32511  nn0min  32973  ccatws1f1o  33090  esplyfvn  33835  fedgmullem2  33888  qqhf  34244  hasheuni  34343  oddpwdc  34612  ballotlemimin  34764  ballotlemfrcn0  34788  bnj1388  35292  prv1n  35745  efrunt  36027  dfon2lem4  36098  dfon2lem7  36101  nmulprop  36504  nandsym1  36746  atbase  39877  llnbase  40097  lplnbase  40122  lvolbase  40166  dalem48  40308  lhpbase  40586  cdlemg17pq  41260  cdlemg19  41272  cdlemg21  41274  dvh3dim3N  42037  fimgmcyc  43116  rmspecnonsq  43448  setindtr  43565  flcidc  43711  omssrncard  44080  scotteld  44786  fmul01lt1lem2  46125  icccncfext  46425  stoweidlem14  46552  stoweidlem26  46564  stirlinglem5  46616  fourierdlem42  46687  fourierdlem62  46706  fourierdlem66  46710  hoicvr  47086  chnsubseq  47420