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  2771  fr3nr  7775  omopthi  8654  cofonr  8667  inf3lem6  9618  rankxpsuc  9880  scotteld  9928  cflim2  10322  ssfin4  10369  fin23lem30  10401  isf32lem5  10416  gchhar  10745  qextlt  13314  qextle  13315  fzneuz  13722  vdwnn  17156  psgnunilem3  19690  efgredlemb  19940  gsumzsplit  20121  lspexchn2  21389  lspindp2l  21392  lspindp2  21393  psrlidm  22249  mplcoe1  22326  mplcoe5  22329  ptopn2  23883  regr1lem2  24039  rnelfmlem  24251  hauspwpwf1  24286  tsmssplit  24451  reconn  25128  itg2splitlem  26049  itg2split  26050  itg2cn  26064  wilthlem2  27378  bposlem9  27601  2sqcoprm  27744  elntg2  29545  nfrgr2v  30855  hatomistici  32946  nn0min  33394  ccatws1f1o  33496  esplyfvn  34191  fedgmullem2  34244  qqhf  34600  hasheuni  34699  oddpwdc  34969  ballotlemimin  35121  ballotlemfrcn0  35145  bnj1388  35646  prv1n  36165  efrunt  36447  dfon2lem4  36518  dfon2lem7  36521  nmulprop  36909  nandsym1  37180  atbase  40314  llnbase  40534  lplnbase  40559  lvolbase  40603  dalem48  40745  lhpbase  41023  cdlemg17pq  41697  cdlemg19  41709  cdlemg21  41711  dvh3dim3N  42474  fimgmcyc  43560  rmspecnonsq  43867  setindtr  43984  flcidc  44130  omssrncard  44499  fmul01lt1lem2  46541  icccncfext  46841  stoweidlem14  46968  stoweidlem26  46980  stirlinglem5  47032  fourierdlem42  47103  fourierdlem62  47122  fourierdlem66  47126  hoicvr  47502