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 ⊢ (𝜑 → ¬ 𝜒)

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

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 210

This theorem is referenced by:  sylnibr  332  neqcomd  2775  fr3nr  7759  omopthi  8635  cofonr  8648  inf3lem6  9590  rankxpsuc  9842  scotteld  9860  cflim2  10235  ssfin4  10282  fin23lem30  10314  isf32lem5  10329  gchhar  10652  qextlt  13220  qextle  13221  fzneuz  13627  vdwnn  17048  psgnunilem3  19557  efgredlemb  19807  gsumzsplit  19988  lspexchn2  21224  lspindp2l  21227  lspindp2  21228  psrlidm  22071  mplcoe1  22148  mplcoe5  22151  ptopn2  23702  regr1lem2  23858  rnelfmlem  24070  hauspwpwf1  24105  tsmssplit  24270  reconn  24947  itg2splitlem  25868  itg2split  25869  itg2cn  25883  wilthlem2  27191  bposlem9  27414  2sqcoprm  27557  elntg2  29244  nfrgr2v  30532  hatomistici  32623  nn0min  33078  ccatws1f1o  33184  esplyfvn  33884  fedgmullem2  33937  qqhf  34293  hasheuni  34392  oddpwdc  34661  ballotlemimin  34813  ballotlemfrcn0  34837  bnj1388  35338  prv1n  35794  efrunt  36076  dfon2lem4  36147  dfon2lem7  36150  nmulprop  36553  nandsym1  36795  atbase  39925  llnbase  40145  lplnbase  40170  lvolbase  40214  dalem48  40356  lhpbase  40634  cdlemg17pq  41308  cdlemg19  41320  cdlemg21  41322  dvh3dim3N  42085  fimgmcyc  43164  rmspecnonsq  43496  setindtr  43613  flcidc  43759  omssrncard  44128  fmul01lt1lem2  46159  icccncfext  46459  stoweidlem14  46586  stoweidlem26  46598  stirlinglem5  46650  fourierdlem42  46721  fourierdlem62  46740  fourierdlem66  46744  hoicvr  47120  chnsubseq  47454