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 195

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 196

This theorem is referenced by:  sylnibr  318  ssnelpss  3680  fr3nr  6871  omopthi  7624  inf3lem6  8413  rankxpsuc  8628  cflim2  8968  ssfin4  9015  fin23lem30  9047  isf32lem5  9062  gchhar  9380  qextlt  11908  qextle  11909  fzneuz  12290  vdwnn  15540  psgnunilem3  17739  efgredlemb  17982  gsumzsplit  18150  lspexchn2  18952  lspindp2l  18955  lspindp2  18956  psrlidm  19224  mplcoe1  19286  mplcoe5  19289  evlslem1  19336  ptopn2  21197  regr1lem2  21353  rnelfmlem  21566  hauspwpwf1  21601  tsmssplit  21765  reconn  22439  itg2splitlem  23321  itg2split  23322  itg2cn  23336  wilthlem2  24595  bposlem9  24817  frgra2v  26526  hatomistici  28605  nn0min  28954  2sqcoprm  28978  qqhf  29358  hasheuni  29474  oddpwdc  29743  ballotlemimin  29894  ballotlemfrcn0  29918  bnj1388  30355  efrunt  30844  dfon2lem4  30935  dfon2lem7  30938  nofulllem5  31105  nandsym1  31591  atbase  33594  llnbase  33813  lplnbase  33838  lvolbase  33882  dalem48  34024  lhpbase  34302  cdlemg17pq  34978  cdlemg19  34990  cdlemg21  34992  dvh3dim3N  35756  rmspecnonsq  36490  setindtr  36609  flcidc  36763  fmul01lt1lem2  38652  icccncfext  38773  stoweidlem14  38907  stoweidlem26  38919  stirlinglem5  38971  fourierdlem42  39042  fourierdlem62  39061  fourierdlem66  39065  hoicvr  39438  nfrgr2v  41442