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  2739  ssnelpss  4067  fr3nr  7712  omopthi  8586  cofonr  8599  inf3lem6  9548  rankxpsuc  9797  cflim2  10176  ssfin4  10223  fin23lem30  10255  isf32lem5  10270  gchhar  10592  qextlt  13123  qextle  13124  fzneuz  13529  vdwnn  16928  psgnunilem3  19393  efgredlemb  19643  gsumzsplit  19824  lspexchn2  21056  lspindp2l  21059  lspindp2  21060  psrlidm  21887  mplcoe1  21960  mplcoe5  21963  ptopn2  23487  regr1lem2  23643  rnelfmlem  23855  hauspwpwf1  23890  tsmssplit  24055  reconn  24733  itg2splitlem  25665  itg2split  25666  itg2cn  25680  wilthlem2  26995  bposlem9  27219  2sqcoprm  27362  elntg2  28948  nfrgr2v  30234  hatomistici  32324  nn0min  32778  ccatws1f1o  32906  fedgmullem2  33602  qqhf  33952  hasheuni  34051  oddpwdc  34321  ballotlemimin  34473  ballotlemfrcn0  34497  bnj1388  34999  prv1n  35403  efrunt  35685  dfon2lem4  35759  dfon2lem7  35762  nandsym1  36395  atbase  39267  llnbase  39488  lplnbase  39513  lvolbase  39557  dalem48  39699  lhpbase  39977  cdlemg17pq  40651  cdlemg19  40663  cdlemg21  40665  dvh3dim3N  41428  fimgmcyc  42507  rmspecnonsq  42880  setindtr  42997  flcidc  43143  omssrncard  43513  scotteld  44219  fmul01lt1lem2  45567  icccncfext  45869  stoweidlem14  45996  stoweidlem26  46008  stirlinglem5  46060  fourierdlem42  46131  fourierdlem62  46150  fourierdlem66  46154  hoicvr  46530