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  2743  ssnelpss  4063  fr3nr  7711  omopthi  8582  cofonr  8595  inf3lem6  9530  rankxpsuc  9782  cflim2  10161  ssfin4  10208  fin23lem30  10240  isf32lem5  10255  gchhar  10577  qextlt  13104  qextle  13105  fzneuz  13510  vdwnn  16912  psgnunilem3  19410  efgredlemb  19660  gsumzsplit  19841  lspexchn2  21070  lspindp2l  21073  lspindp2  21074  psrlidm  21900  mplcoe1  21973  mplcoe5  21976  ptopn2  23500  regr1lem2  23656  rnelfmlem  23868  hauspwpwf1  23903  tsmssplit  24068  reconn  24745  itg2splitlem  25677  itg2split  25678  itg2cn  25692  wilthlem2  27007  bposlem9  27231  2sqcoprm  27374  elntg2  28965  nfrgr2v  30254  hatomistici  32344  nn0min  32808  ccatws1f1o  32939  fedgmullem2  33664  qqhf  34020  hasheuni  34119  oddpwdc  34388  ballotlemimin  34540  ballotlemfrcn0  34564  bnj1388  35066  prv1n  35496  efrunt  35778  dfon2lem4  35849  dfon2lem7  35852  nandsym1  36487  atbase  39408  llnbase  39628  lplnbase  39653  lvolbase  39697  dalem48  39839  lhpbase  40117  cdlemg17pq  40791  cdlemg19  40803  cdlemg21  40805  dvh3dim3N  41568  fimgmcyc  42652  rmspecnonsq  43024  setindtr  43141  flcidc  43287  omssrncard  43657  scotteld  44363  fmul01lt1lem2  45709  icccncfext  46009  stoweidlem14  46136  stoweidlem26  46148  stirlinglem5  46200  fourierdlem42  46271  fourierdlem62  46290  fourierdlem66  46294  hoicvr  46670  chnsubseq  47002