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  2770  fr3nr  7786  omopthi  8673  cofonr  8686  inf3lem6  9637  rankxpsuc  9902  scotteld  9950  cflim2  10344  ssfin4  10391  fin23lem30  10423  isf32lem5  10438  gchhar  10767  qextlt  13336  qextle  13337  fzneuz  13745  vdwnn  17181  psgnunilem3  19715  efgredlemb  19965  gsumzsplit  20146  lspexchn2  21414  lspindp2l  21417  lspindp2  21418  psrlidm  22274  mplcoe1  22351  mplcoe5  22354  ptopn2  23908  regr1lem2  24064  rnelfmlem  24276  hauspwpwf1  24311  tsmssplit  24476  reconn  25153  itg2splitlem  26074  itg2split  26075  itg2cn  26089  wilthlem2  27401  bposlem9  27624  2sqcoprm  27767  nna4b4nsq  27995  elntg2  29568  nfrgr2v  30878  hatomistici  32969  nn0min  33458  ccatws1f1o  33560  esplyfvn  34255  fedgmullem2  34308  qqhf  34664  hasheuni  34763  oddpwdc  35032  ballotlemimin  35184  ballotlemfrcn0  35208  bnj1388  35709  acwer1prc  35816  prv1n  36282  mirimanoffr  36546  efrunt  36570  dfon2lem4  36640  dfon2lem7  36643  nmulprop  37031  nandsym1  37302  atbase  40439  llnbase  40659  lplnbase  40684  lvolbase  40728  dalem48  40870  lhpbase  41148  cdlemg17pq  41822  cdlemg19  41834  cdlemg21  41836  dvh3dim3N  42599  fimgmcyc  43691  rmspecnonsq  44007  setindtr  44124  flcidc  44265  omssrncard  44634  fmul01lt1lem2  46690  icccncfext  46990  stoweidlem14  47117  stoweidlem26  47129  stirlinglem5  47181  fourierdlem42  47252  fourierdlem62  47271  fourierdlem66  47275  hoicvr  47651