Theorem sylnib 320

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

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

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 199

This theorem is referenced by:  sylnibr  321  ssnelpss  3979  fr3nr  7310  omopthi  8084  inf3lem6  8890  rankxpsuc  9105  cflim2  9483  ssfin4  9530  fin23lem30  9562  isf32lem5  9577  gchhar  9899  qextlt  12413  qextle  12414  fzneuz  12804  vdwnn  16190  psgnunilem3  18386  efgredlemb  18631  gsumzsplit  18800  lspexchn2  19625  lspindp2l  19628  lspindp2  19629  psrlidm  19897  mplcoe1  19959  mplcoe5  19962  evlslem1  20008  ptopn2  21896  regr1lem2  22052  rnelfmlem  22264  hauspwpwf1  22299  tsmssplit  22463  reconn  23139  itg2splitlem  24052  itg2split  24053  itg2cn  24067  wilthlem2  25348  bposlem9  25570  2sqcoprm  25713  elntg2  26474  nfrgr2v  27806  hatomistici  29920  nn0min  30283  cycpm2tr  30448  fedgmullem2  30652  qqhf  30868  hasheuni  30985  oddpwdc  31254  ballotlemimin  31406  ballotlemfrcn0  31430  bnj1388  31947  efrunt  32456  dfon2lem4  32548  dfon2lem7  32551  nandsym1  33287  atbase  35867  llnbase  36087  lplnbase  36112  lvolbase  36156  dalem48  36298  lhpbase  36576  cdlemg17pq  37250  cdlemg19  37262  cdlemg21  37264  dvh3dim3N  38027  rmspecnonsq  38897  setindtr  39014  flcidc  39167  neqcomd  39918  scotteld  39954  fmul01lt1lem2  41295  icccncfext  41598  stoweidlem14  41728  stoweidlem26  41740  stirlinglem5  41792  fourierdlem42  41863  fourierdlem62  41882  fourierdlem66  41886  hoicvr  42259