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  2743  ssnelpss  4112  fr3nr  7759  omopthi  8660  cofonr  8673  inf3lem6  9628  rankxpsuc  9877  cflim2  10258  ssfin4  10305  fin23lem30  10337  isf32lem5  10352  gchhar  10674  qextlt  13182  qextle  13183  fzneuz  13582  vdwnn  16931  psgnunilem3  19364  efgredlemb  19614  gsumzsplit  19795  lspexchn2  20744  lspindp2l  20747  lspindp2  20748  psrlidm  21523  mplcoe1  21592  mplcoe5  21595  ptopn2  23088  regr1lem2  23244  rnelfmlem  23456  hauspwpwf1  23491  tsmssplit  23656  reconn  24344  itg2splitlem  25266  itg2split  25267  itg2cn  25281  wilthlem2  26573  bposlem9  26795  2sqcoprm  26938  elntg2  28274  nfrgr2v  29556  hatomistici  31646  nn0min  32057  fedgmullem2  32746  qqhf  32997  hasheuni  33114  oddpwdc  33384  ballotlemimin  33535  ballotlemfrcn0  33559  bnj1388  34075  prv1n  34453  efrunt  34713  dfon2lem4  34789  dfon2lem7  34792  nandsym1  35355  atbase  38207  llnbase  38428  lplnbase  38453  lvolbase  38497  dalem48  38639  lhpbase  38917  cdlemg17pq  39591  cdlemg19  39603  cdlemg21  39605  dvh3dim3N  40368  rmspecnonsq  41693  setindtr  41811  flcidc  41964  omssrncard  42339  scotteld  43053  fmul01lt1lem2  44349  icccncfext  44651  stoweidlem14  44778  stoweidlem26  44790  stirlinglem5  44842  fourierdlem42  44913  fourierdlem62  44932  fourierdlem66  44936  hoicvr  45312