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 227	. 2 ⊢ (𝜒 → 𝜓)
4	1, 3	nsyl 140	1 ⊢ (𝜑 → ¬ 𝜒)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  sylnibr  329  neqcomd  2743  ssnelpss  4112  fr3nr  7759  omopthi  8660  cofonr  8673  inf3lem6  9628  rankxpsuc  9877  cflim2  10258  ssfin4  10305  fin23lem30  10337  isf32lem5  10352  gchhar  10674  qextlt  13182  qextle  13183  fzneuz  13582  vdwnn  16931  psgnunilem3  19364  efgredlemb  19614  gsumzsplit  19795  lspexchn2  20744  lspindp2l  20747  lspindp2  20748  psrlidm  21523  mplcoe1  21592  mplcoe5  21595  ptopn2  23088  regr1lem2  23244  rnelfmlem  23456  hauspwpwf1  23491  tsmssplit  23656  reconn  24344  itg2splitlem  25266  itg2split  25267  itg2cn  25281  wilthlem2  26573  bposlem9  26795  2sqcoprm  26938  elntg2  28243  nfrgr2v  29525  hatomistici  31615  nn0min  32026  fedgmullem2  32715  qqhf  32966  hasheuni  33083  oddpwdc  33353  ballotlemimin  33504  ballotlemfrcn0  33528  bnj1388  34044  prv1n  34422  efrunt  34682  dfon2lem4  34758  dfon2lem7  34761  nandsym1  35307  atbase  38159  llnbase  38380  lplnbase  38405  lvolbase  38449  dalem48  38591  lhpbase  38869  cdlemg17pq  39543  cdlemg19  39555  cdlemg21  39557  dvh3dim3N  40320  rmspecnonsq  41645  setindtr  41763  flcidc  41916  omssrncard  42291  scotteld  43005  fmul01lt1lem2  44301  icccncfext  44603  stoweidlem14  44730  stoweidlem26  44742  stirlinglem5  44794  fourierdlem42  44865  fourierdlem62  44884  fourierdlem66  44888  hoicvr  45264