Theorem sylnib 327

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  328  neqcomd  2748  ssnelpss  4042  fr3nr  7600  omopthi  8451  inf3lem6  9321  rankxpsuc  9571  cflim2  9950  ssfin4  9997  fin23lem30  10029  isf32lem5  10044  gchhar  10366  qextlt  12866  qextle  12867  fzneuz  13266  vdwnn  16627  psgnunilem3  19019  efgredlemb  19267  gsumzsplit  19443  lspexchn2  20308  lspindp2l  20311  lspindp2  20312  psrlidm  21082  mplcoe1  21148  mplcoe5  21151  ptopn2  22643  regr1lem2  22799  rnelfmlem  23011  hauspwpwf1  23046  tsmssplit  23211  reconn  23897  itg2splitlem  24818  itg2split  24819  itg2cn  24833  wilthlem2  26123  bposlem9  26345  2sqcoprm  26488  elntg2  27256  nfrgr2v  28537  hatomistici  30625  nn0min  31036  fedgmullem2  31613  qqhf  31836  hasheuni  31953  oddpwdc  32221  ballotlemimin  32372  ballotlemfrcn0  32396  bnj1388  32913  prv1n  33293  efrunt  33554  dfon2lem4  33668  dfon2lem7  33671  nandsym1  34538  atbase  37230  llnbase  37450  lplnbase  37475  lvolbase  37519  dalem48  37661  lhpbase  37939  cdlemg17pq  38613  cdlemg19  38625  cdlemg21  38627  dvh3dim3N  39390  rmspecnonsq  40645  setindtr  40762  flcidc  40915  scotteld  41753  fmul01lt1lem2  43016  icccncfext  43318  stoweidlem14  43445  stoweidlem26  43457  stirlinglem5  43509  fourierdlem42  43580  fourierdlem62  43599  fourierdlem66  43603  hoicvr  43976