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  2750  ssnelpss  4051  fr3nr  7616  omopthi  8474  inf3lem6  9369  rankxpsuc  9641  cflim2  10020  ssfin4  10067  fin23lem30  10099  isf32lem5  10114  gchhar  10436  qextlt  12936  qextle  12937  fzneuz  13336  vdwnn  16697  psgnunilem3  19102  efgredlemb  19350  gsumzsplit  19526  lspexchn2  20391  lspindp2l  20394  lspindp2  20395  psrlidm  21170  mplcoe1  21236  mplcoe5  21239  ptopn2  22733  regr1lem2  22889  rnelfmlem  23101  hauspwpwf1  23136  tsmssplit  23301  reconn  23989  itg2splitlem  24911  itg2split  24912  itg2cn  24926  wilthlem2  26216  bposlem9  26438  2sqcoprm  26581  elntg2  27351  nfrgr2v  28632  hatomistici  30720  nn0min  31130  fedgmullem2  31707  qqhf  31932  hasheuni  32049  oddpwdc  32317  ballotlemimin  32468  ballotlemfrcn0  32492  bnj1388  33009  prv1n  33389  efrunt  33650  dfon2lem4  33758  dfon2lem7  33761  nandsym1  34607  atbase  37299  llnbase  37519  lplnbase  37544  lvolbase  37588  dalem48  37730  lhpbase  38008  cdlemg17pq  38682  cdlemg19  38694  cdlemg21  38696  dvh3dim3N  39459  rmspecnonsq  40726  setindtr  40843  flcidc  40996  scotteld  41834  fmul01lt1lem2  43097  icccncfext  43399  stoweidlem14  43526  stoweidlem26  43538  stirlinglem5  43590  fourierdlem42  43661  fourierdlem62  43680  fourierdlem66  43684  hoicvr  44057