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  2750  ssnelpss  4137  fr3nr  7807  omopthi  8717  cofonr  8730  inf3lem6  9702  rankxpsuc  9951  cflim2  10332  ssfin4  10379  fin23lem30  10411  isf32lem5  10426  gchhar  10748  qextlt  13265  qextle  13266  fzneuz  13665  vdwnn  17045  psgnunilem3  19538  efgredlemb  19788  gsumzsplit  19969  lspexchn2  21156  lspindp2l  21159  lspindp2  21160  psrlidm  22005  mplcoe1  22078  mplcoe5  22081  ptopn2  23613  regr1lem2  23769  rnelfmlem  23981  hauspwpwf1  24016  tsmssplit  24181  reconn  24869  itg2splitlem  25803  itg2split  25804  itg2cn  25818  wilthlem2  27130  bposlem9  27354  2sqcoprm  27497  elntg2  29018  nfrgr2v  30304  hatomistici  32394  nn0min  32824  ccatws1f1o  32918  fedgmullem2  33643  qqhf  33932  hasheuni  34049  oddpwdc  34319  ballotlemimin  34470  ballotlemfrcn0  34494  bnj1388  35009  prv1n  35399  efrunt  35675  dfon2lem4  35750  dfon2lem7  35753  nandsym1  36388  atbase  39245  llnbase  39466  lplnbase  39491  lvolbase  39535  dalem48  39677  lhpbase  39955  cdlemg17pq  40629  cdlemg19  40641  cdlemg21  40643  dvh3dim3N  41406  fimgmcyc  42489  rmspecnonsq  42863  setindtr  42981  flcidc  43131  omssrncard  43502  scotteld  44215  fmul01lt1lem2  45506  icccncfext  45808  stoweidlem14  45935  stoweidlem26  45947  stirlinglem5  45999  fourierdlem42  46070  fourierdlem62  46089  fourierdlem66  46093  hoicvr  46469