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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  sylnibr  332  neqcomd  2776  fr3nr  7780  omopthi  8656  cofonr  8669  inf3lem6  9612  rankxpsuc  9864  scotteld  9886  cflim2  10265  ssfin4  10312  fin23lem30  10344  isf32lem5  10359  gchhar  10682  qextlt  13247  qextle  13248  fzneuz  13655  vdwnn  17083  psgnunilem3  19597  efgredlemb  19847  gsumzsplit  20028  lspexchn2  21292  lspindp2l  21295  lspindp2  21296  psrlidm  22148  mplcoe1  22225  mplcoe5  22228  ptopn2  23778  regr1lem2  23934  rnelfmlem  24146  hauspwpwf1  24181  tsmssplit  24346  reconn  25023  itg2splitlem  25944  itg2split  25945  itg2cn  25959  wilthlem2  27270  bposlem9  27493  2sqcoprm  27636  elntg2  29372  nfrgr2v  30660  hatomistici  32751  nn0min  33202  ccatws1f1o  33304  esplyfvn  33998  fedgmullem2  34051  qqhf  34407  hasheuni  34506  oddpwdc  34775  ballotlemimin  34927  ballotlemfrcn0  34951  bnj1388  35452  prv1n  35943  efrunt  36225  dfon2lem4  36296  dfon2lem7  36299  nmulprop  36702  nandsym1  36973  atbase  40103  llnbase  40323  lplnbase  40348  lvolbase  40392  dalem48  40534  lhpbase  40812  cdlemg17pq  41486  cdlemg19  41498  cdlemg21  41500  dvh3dim3N  42263  fimgmcyc  43342  rmspecnonsq  43674  setindtr  43791  flcidc  43937  omssrncard  44306  fmul01lt1lem2  46341  icccncfext  46641  stoweidlem14  46768  stoweidlem26  46780  stirlinglem5  46832  fourierdlem42  46903  fourierdlem62  46922  fourierdlem66  46926  hoicvr  47302  chnsubseq  47636