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  2739  ssnelpss  4077  fr3nr  7748  omopthi  8625  cofonr  8638  inf3lem6  9586  rankxpsuc  9835  cflim2  10216  ssfin4  10263  fin23lem30  10295  isf32lem5  10310  gchhar  10632  qextlt  13163  qextle  13164  fzneuz  13569  vdwnn  16969  psgnunilem3  19426  efgredlemb  19676  gsumzsplit  19857  lspexchn2  21041  lspindp2l  21044  lspindp2  21045  psrlidm  21871  mplcoe1  21944  mplcoe5  21947  ptopn2  23471  regr1lem2  23627  rnelfmlem  23839  hauspwpwf1  23874  tsmssplit  24039  reconn  24717  itg2splitlem  25649  itg2split  25650  itg2cn  25664  wilthlem2  26979  bposlem9  27203  2sqcoprm  27346  elntg2  28912  nfrgr2v  30201  hatomistici  32291  nn0min  32745  ccatws1f1o  32873  fedgmullem2  33626  qqhf  33976  hasheuni  34075  oddpwdc  34345  ballotlemimin  34497  ballotlemfrcn0  34521  bnj1388  35023  prv1n  35418  efrunt  35700  dfon2lem4  35774  dfon2lem7  35777  nandsym1  36410  atbase  39282  llnbase  39503  lplnbase  39528  lvolbase  39572  dalem48  39714  lhpbase  39992  cdlemg17pq  40666  cdlemg19  40678  cdlemg21  40680  dvh3dim3N  41443  fimgmcyc  42522  rmspecnonsq  42895  setindtr  43013  flcidc  43159  omssrncard  43529  scotteld  44235  fmul01lt1lem2  45583  icccncfext  45885  stoweidlem14  46012  stoweidlem26  46024  stirlinglem5  46076  fourierdlem42  46147  fourierdlem62  46166  fourierdlem66  46170  hoicvr  46546