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  3751  fr3nr  7021  omopthi  7782  inf3lem6  8568  rankxpsuc  8783  cflim2  9123  ssfin4  9170  fin23lem30  9202  isf32lem5  9217  gchhar  9539  qextlt  12072  qextle  12073  fzneuz  12459  vdwnn  15749  psgnunilem3  17962  efgredlemb  18205  gsumzsplit  18373  lspexchn2  19179  lspindp2l  19182  lspindp2  19183  psrlidm  19451  mplcoe1  19513  mplcoe5  19516  evlslem1  19563  ptopn2  21435  regr1lem2  21591  rnelfmlem  21803  hauspwpwf1  21838  tsmssplit  22002  reconn  22678  itg2splitlem  23560  itg2split  23561  itg2cn  23575  wilthlem2  24840  bposlem9  25062  nfrgr2v  27252  hatomistici  29349  nn0min  29695  2sqcoprm  29775  qqhf  30158  hasheuni  30275  oddpwdc  30544  ballotlemimin  30695  ballotlemfrcn0  30719  bnj1388  31227  efrunt  31716  dfon2lem4  31815  dfon2lem7  31818  nandsym1  32546  atbase  34894  llnbase  35113  lplnbase  35138  lvolbase  35182  dalem48  35324  lhpbase  35602  cdlemg17pq  36277  cdlemg19  36289  cdlemg21  36291  dvh3dim3N  37055  rmspecnonsq  37789  setindtr  37908  flcidc  38061  fmul01lt1lem2  40135  icccncfext  40418  stoweidlem14  40549  stoweidlem26  40561  stirlinglem5  40613  fourierdlem42  40684  fourierdlem62  40703  fourierdlem66  40707  hoicvr  41083