Theorem sylnib 317

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	a1i 11	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	1, 3	mtbid 313	1 ⊢ (𝜑 → ¬ 𝜒)

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

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 197

This theorem is referenced by:  sylnibr  318  ssnelpss  3858  fr3nr  7142  omopthi  7904  inf3lem6  8701  rankxpsuc  8916  cflim2  9275  ssfin4  9322  fin23lem30  9354  isf32lem5  9369  gchhar  9691  qextlt  12225  qextle  12226  fzneuz  12612  vdwnn  15902  psgnunilem3  18114  efgredlemb  18357  gsumzsplit  18525  lspexchn2  19331  lspindp2l  19334  lspindp2  19335  psrlidm  19603  mplcoe1  19665  mplcoe5  19668  evlslem1  19715  ptopn2  21587  regr1lem2  21743  rnelfmlem  21955  hauspwpwf1  21990  tsmssplit  22154  reconn  22830  itg2splitlem  23712  itg2split  23713  itg2cn  23727  wilthlem2  24992  bposlem9  25214  nfrgr2v  27424  hatomistici  29528  nn0min  29874  2sqcoprm  29954  qqhf  30337  hasheuni  30454  oddpwdc  30723  ballotlemimin  30874  ballotlemfrcn0  30898  bnj1388  31406  efrunt  31895  dfon2lem4  31994  dfon2lem7  31997  nandsym1  32725  atbase  35077  llnbase  35296  lplnbase  35321  lvolbase  35365  dalem48  35507  lhpbase  35785  cdlemg17pq  36460  cdlemg19  36472  cdlemg21  36474  dvh3dim3N  37238  rmspecnonsq  37972  setindtr  38091  flcidc  38244  fmul01lt1lem2  40318  icccncfext  40601  stoweidlem14  40732  stoweidlem26  40744  stirlinglem5  40796  fourierdlem42  40867  fourierdlem62  40886  fourierdlem66  40890  hoicvr  41266