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  2746  fr3nr  7726  omopthi  8597  cofonr  8610  inf3lem6  9554  rankxpsuc  9806  cflim2  10185  ssfin4  10232  fin23lem30  10264  isf32lem5  10279  gchhar  10602  qextlt  13155  qextle  13156  fzneuz  13562  vdwnn  16969  psgnunilem3  19471  efgredlemb  19721  gsumzsplit  19902  lspexchn2  21129  lspindp2l  21132  lspindp2  21133  psrlidm  21940  mplcoe1  22015  mplcoe5  22018  ptopn2  23549  regr1lem2  23705  rnelfmlem  23917  hauspwpwf1  23952  tsmssplit  24117  reconn  24794  itg2splitlem  25715  itg2split  25716  itg2cn  25730  wilthlem2  27032  bposlem9  27255  2sqcoprm  27398  elntg2  29054  nfrgr2v  30342  hatomistici  32433  nn0min  32894  ccatws1f1o  33011  esplyfvn  33721  fedgmullem2  33774  qqhf  34130  hasheuni  34229  oddpwdc  34498  ballotlemimin  34650  ballotlemfrcn0  34674  bnj1388  35175  prv1n  35613  efrunt  35895  dfon2lem4  35966  dfon2lem7  35969  nandsym1  36604  atbase  39735  llnbase  39955  lplnbase  39980  lvolbase  40024  dalem48  40166  lhpbase  40444  cdlemg17pq  41118  cdlemg19  41130  cdlemg21  41132  dvh3dim3N  41895  fimgmcyc  42979  rmspecnonsq  43335  setindtr  43452  flcidc  43598  omssrncard  43967  scotteld  44673  fmul01lt1lem2  46015  icccncfext  46315  stoweidlem14  46442  stoweidlem26  46454  stirlinglem5  46506  fourierdlem42  46577  fourierdlem62  46596  fourierdlem66  46600  hoicvr  46976  chnsubseq  47310