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  2745  ssnelpss  4089  fr3nr  7766  omopthi  8673  cofonr  8686  inf3lem6  9647  rankxpsuc  9896  cflim2  10277  ssfin4  10324  fin23lem30  10356  isf32lem5  10371  gchhar  10693  qextlt  13219  qextle  13220  fzneuz  13625  vdwnn  17018  psgnunilem3  19477  efgredlemb  19727  gsumzsplit  19908  lspexchn2  21092  lspindp2l  21095  lspindp2  21096  psrlidm  21922  mplcoe1  21995  mplcoe5  21998  ptopn2  23522  regr1lem2  23678  rnelfmlem  23890  hauspwpwf1  23925  tsmssplit  24090  reconn  24768  itg2splitlem  25701  itg2split  25702  itg2cn  25716  wilthlem2  27031  bposlem9  27255  2sqcoprm  27398  elntg2  28964  nfrgr2v  30253  hatomistici  32343  nn0min  32799  ccatws1f1o  32927  fedgmullem2  33670  qqhf  34017  hasheuni  34116  oddpwdc  34386  ballotlemimin  34538  ballotlemfrcn0  34562  bnj1388  35064  prv1n  35453  efrunt  35730  dfon2lem4  35804  dfon2lem7  35807  nandsym1  36440  atbase  39307  llnbase  39528  lplnbase  39553  lvolbase  39597  dalem48  39739  lhpbase  40017  cdlemg17pq  40691  cdlemg19  40703  cdlemg21  40705  dvh3dim3N  41468  fimgmcyc  42557  rmspecnonsq  42930  setindtr  43048  flcidc  43194  omssrncard  43564  scotteld  44270  fmul01lt1lem2  45614  icccncfext  45916  stoweidlem14  46043  stoweidlem26  46055  stirlinglem5  46107  fourierdlem42  46178  fourierdlem62  46197  fourierdlem66  46201  hoicvr  46577