Theorem sylnib 328

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	biimpri 227	. 2 ⊢ (𝜒 → 𝜓)
4	1, 3	nsyl 140	1 ⊢ (𝜑 → ¬ 𝜒)

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

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 206

This theorem is referenced by:  sylnibr  329  neqcomd  2734  ssnelpss  4103  fr3nr  7752  omopthi  8656  cofonr  8669  inf3lem6  9624  rankxpsuc  9873  cflim2  10254  ssfin4  10301  fin23lem30  10333  isf32lem5  10348  gchhar  10670  qextlt  13179  qextle  13180  fzneuz  13579  vdwnn  16930  psgnunilem3  19406  efgredlemb  19656  gsumzsplit  19837  lspexchn2  20972  lspindp2l  20975  lspindp2  20976  psrlidm  21833  mplcoe1  21902  mplcoe5  21905  ptopn2  23410  regr1lem2  23566  rnelfmlem  23778  hauspwpwf1  23813  tsmssplit  23978  reconn  24666  itg2splitlem  25600  itg2split  25601  itg2cn  25615  wilthlem2  26917  bposlem9  27141  2sqcoprm  27284  elntg2  28712  nfrgr2v  29994  hatomistici  32084  nn0min  32493  fedgmullem2  33194  qqhf  33455  hasheuni  33572  oddpwdc  33842  ballotlemimin  33993  ballotlemfrcn0  34017  bnj1388  34533  prv1n  34911  efrunt  35177  dfon2lem4  35253  dfon2lem7  35256  nandsym1  35797  atbase  38649  llnbase  38870  lplnbase  38895  lvolbase  38939  dalem48  39081  lhpbase  39359  cdlemg17pq  40033  cdlemg19  40045  cdlemg21  40047  dvh3dim3N  40810  rmspecnonsq  42134  setindtr  42252  flcidc  42405  omssrncard  42780  scotteld  43494  fmul01lt1lem2  44786  icccncfext  45088  stoweidlem14  45215  stoweidlem26  45227  stirlinglem5  45279  fourierdlem42  45350  fourierdlem62  45369  fourierdlem66  45373  hoicvr  45749