Theorem sylnib 331

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 231	. 2 ⊢ (𝜒 → 𝜓)
4	1, 3	nsyl 142	1 ⊢ (𝜑 → ¬ 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  sylnibr  332  neqcomd  2746  ssnelpss  4012  fr3nr  7535  omopthi  8364  inf3lem6  9226  rankxpsuc  9463  cflim2  9842  ssfin4  9889  fin23lem30  9921  isf32lem5  9936  gchhar  10258  qextlt  12758  qextle  12759  fzneuz  13158  vdwnn  16514  psgnunilem3  18842  efgredlemb  19090  gsumzsplit  19266  lspexchn2  20122  lspindp2l  20125  lspindp2  20126  psrlidm  20882  mplcoe1  20948  mplcoe5  20951  ptopn2  22435  regr1lem2  22591  rnelfmlem  22803  hauspwpwf1  22838  tsmssplit  23003  reconn  23679  itg2splitlem  24600  itg2split  24601  itg2cn  24615  wilthlem2  25905  bposlem9  26127  2sqcoprm  26270  elntg2  27030  nfrgr2v  28309  hatomistici  30397  nn0min  30808  fedgmullem2  31379  qqhf  31602  hasheuni  31719  oddpwdc  31987  ballotlemimin  32138  ballotlemfrcn0  32162  bnj1388  32680  prv1n  33060  efrunt  33321  dfon2lem4  33432  dfon2lem7  33435  nandsym1  34297  atbase  36989  llnbase  37209  lplnbase  37234  lvolbase  37278  dalem48  37420  lhpbase  37698  cdlemg17pq  38372  cdlemg19  38384  cdlemg21  38386  dvh3dim3N  39149  rmspecnonsq  40373  setindtr  40490  flcidc  40643  scotteld  41478  fmul01lt1lem2  42744  icccncfext  43046  stoweidlem14  43173  stoweidlem26  43185  stirlinglem5  43237  fourierdlem42  43308  fourierdlem62  43327  fourierdlem66  43331  hoicvr  43704