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  2746  ssnelpss  4066  fr3nr  7717  omopthi  8589  cofonr  8602  inf3lem6  9542  rankxpsuc  9794  cflim2  10173  ssfin4  10220  fin23lem30  10252  isf32lem5  10267  gchhar  10590  qextlt  13118  qextle  13119  fzneuz  13524  vdwnn  16926  psgnunilem3  19425  efgredlemb  19675  gsumzsplit  19856  lspexchn2  21086  lspindp2l  21089  lspindp2  21090  psrlidm  21917  mplcoe1  21992  mplcoe5  21995  ptopn2  23528  regr1lem2  23684  rnelfmlem  23896  hauspwpwf1  23931  tsmssplit  24096  reconn  24773  itg2splitlem  25705  itg2split  25706  itg2cn  25720  wilthlem2  27035  bposlem9  27259  2sqcoprm  27402  elntg2  29058  nfrgr2v  30347  hatomistici  32437  nn0min  32901  ccatws1f1o  33033  esplyfvn  33733  fedgmullem2  33787  qqhf  34143  hasheuni  34242  oddpwdc  34511  ballotlemimin  34663  ballotlemfrcn0  34687  bnj1388  35189  prv1n  35625  efrunt  35907  dfon2lem4  35978  dfon2lem7  35981  nandsym1  36616  atbase  39545  llnbase  39765  lplnbase  39790  lvolbase  39834  dalem48  39976  lhpbase  40254  cdlemg17pq  40928  cdlemg19  40940  cdlemg21  40942  dvh3dim3N  41705  fimgmcyc  42785  rmspecnonsq  43145  setindtr  43262  flcidc  43408  omssrncard  43777  scotteld  44483  fmul01lt1lem2  45827  icccncfext  46127  stoweidlem14  46254  stoweidlem26  46266  stirlinglem5  46318  fourierdlem42  46389  fourierdlem62  46408  fourierdlem66  46412  hoicvr  46788  chnsubseq  47120