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  2747  ssnelpss  4114  fr3nr  7792  omopthi  8699  cofonr  8712  inf3lem6  9673  rankxpsuc  9922  cflim2  10303  ssfin4  10350  fin23lem30  10382  isf32lem5  10397  gchhar  10719  qextlt  13245  qextle  13246  fzneuz  13648  vdwnn  17036  psgnunilem3  19514  efgredlemb  19764  gsumzsplit  19945  lspexchn2  21133  lspindp2l  21136  lspindp2  21137  psrlidm  21982  mplcoe1  22055  mplcoe5  22058  ptopn2  23592  regr1lem2  23748  rnelfmlem  23960  hauspwpwf1  23995  tsmssplit  24160  reconn  24850  itg2splitlem  25783  itg2split  25784  itg2cn  25798  wilthlem2  27112  bposlem9  27336  2sqcoprm  27479  elntg2  29000  nfrgr2v  30291  hatomistici  32381  nn0min  32822  ccatws1f1o  32936  fedgmullem2  33681  qqhf  33987  hasheuni  34086  oddpwdc  34356  ballotlemimin  34508  ballotlemfrcn0  34532  bnj1388  35047  prv1n  35436  efrunt  35713  dfon2lem4  35787  dfon2lem7  35790  nandsym1  36423  atbase  39290  llnbase  39511  lplnbase  39536  lvolbase  39580  dalem48  39722  lhpbase  40000  cdlemg17pq  40674  cdlemg19  40686  cdlemg21  40688  dvh3dim3N  41451  fimgmcyc  42544  rmspecnonsq  42918  setindtr  43036  flcidc  43182  omssrncard  43553  scotteld  44265  fmul01lt1lem2  45600  icccncfext  45902  stoweidlem14  46029  stoweidlem26  46041  stirlinglem5  46093  fourierdlem42  46164  fourierdlem62  46183  fourierdlem66  46187  hoicvr  46563