Theorem sylnib 316

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

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

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 195

This theorem is referenced by:  sylnibr  317  ssnelpss  3679  fr3nr  6848  omopthi  7601  inf3lem6  8390  rankxpsuc  8605  cflim2  8945  ssfin4  8992  fin23lem30  9024  isf32lem5  9039  gchhar  9357  qextlt  11869  qextle  11870  fzneuz  12247  vdwnn  15488  psgnunilem3  17687  efgredlemb  17930  gsumzsplit  18098  lspexchn2  18900  lspindp2l  18903  lspindp2  18904  psrlidm  19172  mplcoe1  19234  mplcoe5  19237  evlslem1  19284  ptopn2  21144  regr1lem2  21300  rnelfmlem  21513  hauspwpwf1  21548  tsmssplit  21712  reconn  22386  itg2splitlem  23265  itg2split  23266  itg2cn  23280  wilthlem2  24539  bposlem9  24761  frgra2v  26319  hatomistici  28398  nn0min  28747  2sqcoprm  28771  qqhf  29151  hasheuni  29267  oddpwdc  29536  ballotlemimin  29687  ballotlemfrcn0  29711  bnj1388  30148  efrunt  30637  dfon2lem4  30728  dfon2lem7  30731  nofulllem5  30898  nandsym1  31384  atbase  33377  llnbase  33596  lplnbase  33621  lvolbase  33665  dalem48  33807  lhpbase  34085  cdlemg17pq  34761  cdlemg19  34773  cdlemg21  34775  dvh3dim3N  35539  rmspecnonsq  36273  setindtr  36392  flcidc  36546  fmul01lt1lem2  38435  icccncfext  38556  stoweidlem14  38690  stoweidlem26  38702  stirlinglem5  38754  fourierdlem42  38825  fourierdlem62  38844  fourierdlem66  38848  hoicvr  39221  nfrgr2v  41423