Theorem sylnib 331

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  sylnibr  332  neqcomd  2773  fr3nr  7810  omopthi  8698  cofonr  8711  inf3lem6  9661  rankxpsuc  9926  scotteld  9974  cflim2  10368  ssfin4  10415  fin23lem30  10447  isf32lem5  10462  gchhar  10791  qextlt  13360  qextle  13361  fzneuz  13769  vdwnn  17205  psgnunilem3  19740  efgredlemb  19990  gsumzsplit  20171  lspexchn2  21439  lspindp2l  21442  lspindp2  21443  psrlidm  22299  mplcoe1  22376  mplcoe5  22379  ptopn2  23933  regr1lem2  24089  rnelfmlem  24301  hauspwpwf1  24336  tsmssplit  24501  reconn  25178  itg2splitlem  26099  itg2split  26100  itg2cn  26114  wilthlem2  27426  bposlem9  27649  2sqcoprm  27792  nna4b4nsq  28020  elntg2  29593  nfrgr2v  30903  hatomistici  32994  nn0min  33482  ccatws1f1o  33584  esplyfvn  34279  fedgmullem2  34332  qqhf  34688  hasheuni  34787  oddpwdc  35056  ballotlemimin  35208  ballotlemfrcn0  35232  bnj1388  35733  erscottd  35843  acwer1prc  35852  prv1n  36363  mirimanoffr  36627  efrunt  36656  dfon2lem4  36726  dfon2lem7  36729  nmulprop  37117  nandsym1  37388  atbase  40538  llnbase  40758  lplnbase  40783  lvolbase  40827  dalem48  40969  lhpbase  41247  cdlemg17pq  41921  cdlemg19  41933  cdlemg21  41935  dvh3dim3N  42698  fimgmcyc  43791  rmspecnonsq  44107  setindtr  44224  flcidc  44364  omssrncard  44733  fmul01lt1lem2  46802  icccncfext  47102  stoweidlem14  47229  stoweidlem26  47241  stirlinglem5  47293  fourierdlem42  47364  fourierdlem62  47383  fourierdlem66  47387  hoicvr  47763