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  2741  ssnelpss  4064  fr3nr  7705  omopthi  8576  cofonr  8589  inf3lem6  9523  rankxpsuc  9772  cflim2  10151  ssfin4  10198  fin23lem30  10230  isf32lem5  10245  gchhar  10567  qextlt  13099  qextle  13100  fzneuz  13505  vdwnn  16907  psgnunilem3  19406  efgredlemb  19656  gsumzsplit  19837  lspexchn2  21066  lspindp2l  21069  lspindp2  21070  psrlidm  21897  mplcoe1  21970  mplcoe5  21973  ptopn2  23497  regr1lem2  23653  rnelfmlem  23865  hauspwpwf1  23900  tsmssplit  24065  reconn  24742  itg2splitlem  25674  itg2split  25675  itg2cn  25689  wilthlem2  27004  bposlem9  27228  2sqcoprm  27371  elntg2  28961  nfrgr2v  30247  hatomistici  32337  nn0min  32798  ccatws1f1o  32927  fedgmullem2  33638  qqhf  33994  hasheuni  34093  oddpwdc  34362  ballotlemimin  34514  ballotlemfrcn0  34538  bnj1388  35040  prv1n  35463  efrunt  35745  dfon2lem4  35819  dfon2lem7  35822  nandsym1  36455  atbase  39327  llnbase  39547  lplnbase  39572  lvolbase  39616  dalem48  39758  lhpbase  40036  cdlemg17pq  40710  cdlemg19  40722  cdlemg21  40724  dvh3dim3N  41487  fimgmcyc  42566  rmspecnonsq  42939  setindtr  43056  flcidc  43202  omssrncard  43572  scotteld  44278  fmul01lt1lem2  45624  icccncfext  45924  stoweidlem14  46051  stoweidlem26  46063  stirlinglem5  46115  fourierdlem42  46186  fourierdlem62  46205  fourierdlem66  46209  hoicvr  46585