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  fr3nr  7719  omopthi  8590  cofonr  8603  inf3lem6  9545  rankxpsuc  9797  cflim2  10176  ssfin4  10223  fin23lem30  10255  isf32lem5  10270  gchhar  10593  qextlt  13146  qextle  13147  fzneuz  13553  vdwnn  16960  psgnunilem3  19462  efgredlemb  19712  gsumzsplit  19893  lspexchn2  21121  lspindp2l  21124  lspindp2  21125  psrlidm  21950  mplcoe1  22025  mplcoe5  22028  ptopn2  23559  regr1lem2  23715  rnelfmlem  23927  hauspwpwf1  23962  tsmssplit  24127  reconn  24804  itg2splitlem  25725  itg2split  25726  itg2cn  25740  wilthlem2  27046  bposlem9  27269  2sqcoprm  27412  elntg2  29068  nfrgr2v  30357  hatomistici  32448  nn0min  32909  ccatws1f1o  33026  esplyfvn  33736  fedgmullem2  33790  qqhf  34146  hasheuni  34245  oddpwdc  34514  ballotlemimin  34666  ballotlemfrcn0  34690  bnj1388  35191  prv1n  35629  efrunt  35911  dfon2lem4  35982  dfon2lem7  35985  nandsym1  36620  atbase  39749  llnbase  39969  lplnbase  39994  lvolbase  40038  dalem48  40180  lhpbase  40458  cdlemg17pq  41132  cdlemg19  41144  cdlemg21  41146  dvh3dim3N  41909  fimgmcyc  42993  rmspecnonsq  43353  setindtr  43470  flcidc  43616  omssrncard  43985  scotteld  44691  fmul01lt1lem2  46033  icccncfext  46333  stoweidlem14  46460  stoweidlem26  46472  stirlinglem5  46524  fourierdlem42  46595  fourierdlem62  46614  fourierdlem66  46618  hoicvr  46994  chnsubseq  47326