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  2745  ssnelpss  4124  fr3nr  7791  omopthi  8698  cofonr  8711  inf3lem6  9671  rankxpsuc  9920  cflim2  10301  ssfin4  10348  fin23lem30  10380  isf32lem5  10395  gchhar  10717  qextlt  13242  qextle  13243  fzneuz  13645  vdwnn  17032  psgnunilem3  19529  efgredlemb  19779  gsumzsplit  19960  lspexchn2  21151  lspindp2l  21154  lspindp2  21155  psrlidm  22000  mplcoe1  22073  mplcoe5  22076  ptopn2  23608  regr1lem2  23764  rnelfmlem  23976  hauspwpwf1  24011  tsmssplit  24176  reconn  24864  itg2splitlem  25798  itg2split  25799  itg2cn  25813  wilthlem2  27127  bposlem9  27351  2sqcoprm  27494  elntg2  29015  nfrgr2v  30301  hatomistici  32391  nn0min  32827  ccatws1f1o  32921  fedgmullem2  33658  qqhf  33949  hasheuni  34066  oddpwdc  34336  ballotlemimin  34487  ballotlemfrcn0  34511  bnj1388  35026  prv1n  35416  efrunt  35693  dfon2lem4  35768  dfon2lem7  35771  nandsym1  36405  atbase  39271  llnbase  39492  lplnbase  39517  lvolbase  39561  dalem48  39703  lhpbase  39981  cdlemg17pq  40655  cdlemg19  40667  cdlemg21  40669  dvh3dim3N  41432  fimgmcyc  42521  rmspecnonsq  42895  setindtr  43013  flcidc  43159  omssrncard  43530  scotteld  44242  fmul01lt1lem2  45541  icccncfext  45843  stoweidlem14  45970  stoweidlem26  45982  stirlinglem5  46034  fourierdlem42  46105  fourierdlem62  46124  fourierdlem66  46128  hoicvr  46504