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

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

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 206

This theorem is referenced by:  sylnibr  329  neqcomd  2748  ssnelpss  4046  fr3nr  7622  omopthi  8491  inf3lem6  9391  rankxpsuc  9640  cflim2  10019  ssfin4  10066  fin23lem30  10098  isf32lem5  10113  gchhar  10435  qextlt  12937  qextle  12938  fzneuz  13337  vdwnn  16699  psgnunilem3  19104  efgredlemb  19352  gsumzsplit  19528  lspexchn2  20393  lspindp2l  20396  lspindp2  20397  psrlidm  21172  mplcoe1  21238  mplcoe5  21241  ptopn2  22735  regr1lem2  22891  rnelfmlem  23103  hauspwpwf1  23138  tsmssplit  23303  reconn  23991  itg2splitlem  24913  itg2split  24914  itg2cn  24928  wilthlem2  26218  bposlem9  26440  2sqcoprm  26583  elntg2  27353  nfrgr2v  28636  hatomistici  30724  nn0min  31134  fedgmullem2  31711  qqhf  31936  hasheuni  32053  oddpwdc  32321  ballotlemimin  32472  ballotlemfrcn0  32496  bnj1388  33013  prv1n  33393  efrunt  33654  dfon2lem4  33762  dfon2lem7  33765  nandsym1  34611  atbase  37303  llnbase  37523  lplnbase  37548  lvolbase  37592  dalem48  37734  lhpbase  38012  cdlemg17pq  38686  cdlemg19  38698  cdlemg21  38700  dvh3dim3N  39463  rmspecnonsq  40729  setindtr  40846  flcidc  40999  omssrncard  41147  scotteld  41864  fmul01lt1lem2  43126  icccncfext  43428  stoweidlem14  43555  stoweidlem26  43567  stirlinglem5  43619  fourierdlem42  43690  fourierdlem62  43709  fourierdlem66  43713  hoicvr  44086