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 141	1 ⊢ (𝜑 → ¬ 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  sylnibr  332  neqcomd  2772  fr3nr  7775  omopthi  8653  cofonr  8666  inf3lem6  9616  rankxpsuc  9868  scotteld  9890  cflim2  10269  ssfin4  10316  fin23lem30  10348  isf32lem5  10363  gchhar  10692  qextlt  13259  qextle  13260  fzneuz  13667  vdwnn  17096  psgnunilem3  19629  efgredlemb  19879  gsumzsplit  20060  lspexchn2  21324  lspindp2l  21327  lspindp2  21328  psrlidm  22182  mplcoe1  22259  mplcoe5  22262  ptopn2  23816  regr1lem2  23972  rnelfmlem  24184  hauspwpwf1  24219  tsmssplit  24384  reconn  25061  itg2splitlem  25982  itg2split  25983  itg2cn  25997  wilthlem2  27313  bposlem9  27536  2sqcoprm  27679  elntg2  29450  nfrgr2v  30760  hatomistici  32851  nn0min  33299  ccatws1f1o  33401  esplyfvn  34095  fedgmullem2  34148  qqhf  34504  hasheuni  34603  oddpwdc  34873  ballotlemimin  35025  ballotlemfrcn0  35049  bnj1388  35550  prv1n  36018  efrunt  36300  dfon2lem4  36371  dfon2lem7  36374  nmulprop  36778  nandsym1  37049  atbase  40170  llnbase  40390  lplnbase  40415  lvolbase  40459  dalem48  40601  lhpbase  40879  cdlemg17pq  41553  cdlemg19  41565  cdlemg21  41567  dvh3dim3N  42330  fimgmcyc  43424  rmspecnonsq  43756  setindtr  43873  flcidc  44019  omssrncard  44388  fmul01lt1lem2  46423  icccncfext  46723  stoweidlem14  46850  stoweidlem26  46862  stirlinglem5  46914  fourierdlem42  46985  fourierdlem62  47004  fourierdlem66  47008  hoicvr  47384