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  2740  ssnelpss  4080  fr3nr  7751  omopthi  8628  cofonr  8641  inf3lem6  9593  rankxpsuc  9842  cflim2  10223  ssfin4  10270  fin23lem30  10302  isf32lem5  10317  gchhar  10639  qextlt  13170  qextle  13171  fzneuz  13576  vdwnn  16976  psgnunilem3  19433  efgredlemb  19683  gsumzsplit  19864  lspexchn2  21048  lspindp2l  21051  lspindp2  21052  psrlidm  21878  mplcoe1  21951  mplcoe5  21954  ptopn2  23478  regr1lem2  23634  rnelfmlem  23846  hauspwpwf1  23881  tsmssplit  24046  reconn  24724  itg2splitlem  25656  itg2split  25657  itg2cn  25671  wilthlem2  26986  bposlem9  27210  2sqcoprm  27353  elntg2  28919  nfrgr2v  30208  hatomistici  32298  nn0min  32752  ccatws1f1o  32880  fedgmullem2  33633  qqhf  33983  hasheuni  34082  oddpwdc  34352  ballotlemimin  34504  ballotlemfrcn0  34528  bnj1388  35030  prv1n  35425  efrunt  35707  dfon2lem4  35781  dfon2lem7  35784  nandsym1  36417  atbase  39289  llnbase  39510  lplnbase  39535  lvolbase  39579  dalem48  39721  lhpbase  39999  cdlemg17pq  40673  cdlemg19  40685  cdlemg21  40687  dvh3dim3N  41450  fimgmcyc  42529  rmspecnonsq  42902  setindtr  43020  flcidc  43166  omssrncard  43536  scotteld  44242  fmul01lt1lem2  45590  icccncfext  45892  stoweidlem14  46019  stoweidlem26  46031  stirlinglem5  46083  fourierdlem42  46154  fourierdlem62  46173  fourierdlem66  46177  hoicvr  46553