Theorem sylnibr 331

Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)

Hypotheses

Ref	Expression
sylnibr.1	⊢ (𝜑 → ¬ 𝜓)
sylnibr.2	⊢ (𝜒 ↔ 𝜓)

Assertion

Ref	Expression
sylnibr	⊢ (𝜑 → ¬ 𝜒)

Proof of Theorem sylnibr

Step	Hyp	Ref	Expression
1		sylnibr.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		sylnibr.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	2	bicomi 226	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	sylnib 330	1 ⊢ (𝜑 → ¬ 𝜒)

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

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 209

This theorem is referenced by:  jcndOLD  339  otiunsndisj  5410  pofun  5491  disjen  8674  php3  8703  sdom1  8718  wemappo  9013  cnfcom2lem  9164  zfregs2  9175  cfsuc  9679  fin1a2lem12  9833  ac6num  9901  canth4  10069  pwfseqlem3  10082  gchpwdom  10092  gchaleph  10093  gchhar  10101  difreicc  12871  fzpreddisj  12957  ccatalpha  13947  s3iunsndisj  14328  fprodntriv  15296  fprodn0f  15345  lcmfunsnlem2lem2  15983  prmreclem5  16256  cidpropd  16980  gsumpropd2lem  17889  isnsgrp  17905  isnmnd  17915  mulgfval  18226  odinf  18690  frgpnabllem1  18993  ablfac1lem  19190  ablsimpgfindlem2  19230  frlmssuvc2  20939  lmmo  21988  xkohaus  22261  snfil  22472  supfil  22503  hauspwpwf1  22595  tsmsfbas  22736  reconnlem2  23435  minveclem3b  24031  dvply1  24873  taylthlem2  24962  wilthlem2  25646  lgseisenlem1  25951  axlowdimlem6  26733  elntg2  26771  structiedg0val  26807  snstriedgval  26823  incistruhgr  26864  umgr2edg1  26993  umgr2edgneu  26996  wlkp1lem1  27455  eupth2eucrct  27996  4cycl2vnunb  28069  frgrncvvdeqlem1  28078  n0lplig  28260  addsqnot2reu  30249  ssmxidllem  30978  qqhf  31227  hgt750lemb  31927  bnj1417  32313  subfacp1lem1  32426  fmlasucdisj  32646  prv0  32677  pocnv  32999  wsuclb  33115  nosepon  33172  filnetlem4  33729  bj-ab0  34227  topdifinffinlem  34631  relowlpssretop  34648  finxpnom  34685  heibor1lem  35102  notornotel2  35389  pmap0  36916  mapdh6eN  38891  mapdh7dN  38901  hdmap1l6e  38965  negn0nposznnd  39217  jm2.23  39642  rpnnen3lem  39677  fnwe2lem2  39700  fzdifsuc2  41626  icoiccdif  41849  climrec  41933  sumnnodd  41960  lptioo2  41961  lptioo1  41962  limcresiooub  41972  limcresioolb  41973  icccncfext  42219  cncfiooicclem1  42225  dvmptfprodlem  42278  stoweidlem34  42368  stoweidlem39  42373  stoweidlem59  42393  stirlinglem8  42415  dirkercncflem2  42438  fourierdlem12  42453  fourierdlem40  42481  fourierdlem42  42483  fourierdlem48  42488  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem78  42518  fourierdlem93  42533  fourierdlem103  42543  fourierdlem104  42544  elaa2  42568  sge0split  42740  iundjiun  42791  meaiininclem  42817  preimagelt  43029  preimalegt  43030  otiunsndisjX  43527  fun2dmnopgexmpl  43532  0nelsetpreimafv  43599  ichnreuop  43683  0nodd  44126  cznnring  44276