Theorem sylnibr 328

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 223	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	sylnib 327	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:  jcndOLD  336  otiunsndisj  5436  pofun  5520  disjen  8886  php3  8959  php3OLD  8972  sdom1  8984  wemappo  9269  cnfcom2lem  9420  zfregs2  9474  cfsuc  9997  fin1a2lem12  10151  ac6num  10219  canth4  10387  pwfseqlem3  10400  gchpwdom  10410  gchaleph  10411  gchhar  10419  difreicc  13198  fzpreddisj  13287  ccatalpha  14279  s3iunsndisj  14660  fprodntriv  15633  fprodn0f  15682  lcmfunsnlem2lem2  16325  prmreclem5  16602  cidpropd  17400  gsumpropd2lem  18344  isnsgrp  18360  isnmnd  18370  mulgfval  18683  odinf  19151  frgpnabllem1  19455  ablfac1lem  19652  ablsimpgfindlem2  19692  frlmssuvc2  20983  lmmo  22512  xkohaus  22785  snfil  22996  supfil  23027  hauspwpwf1  23119  tsmsfbas  23260  reconnlem2  23971  minveclem3b  24573  dvply1  25425  taylthlem2  25514  wilthlem2  26199  lgseisenlem1  26504  axlowdimlem6  27296  elntg2  27334  structiedg0val  27373  snstriedgval  27389  incistruhgr  27430  umgr2edg1  27559  umgr2edgneu  27562  wlkp1lem1  28021  eupth2eucrct  28560  4cycl2vnunb  28633  frgrncvvdeqlem1  28642  n0lplig  28824  addsqnot2reu  30813  ssmxidllem  31620  qqhf  31915  hgt750lemb  32615  bnj1417  33000  subfacp1lem1  33120  fmlasucdisj  33340  prv0  33371  pocnv  33709  wsuclb  33801  nosepon  33847  filnetlem4  34549  bj-ab0  35072  topdifinffinlem  35497  relowlpssretop  35514  finxpnom  35551  heibor1lem  35946  notornotel2  36233  pmap0  37758  mapdh6eN  39733  mapdh7dN  39743  hdmap1l6e  39807  dvrelogpow2b  40056  aks4d1p1p4  40059  negn0nposznnd  40290  jm2.23  40798  rpnnen3lem  40833  fnwe2lem2  40856  imsqrtvalex  41207  fzdifsuc2  42803  icoiccdif  43016  climrec  43098  sumnnodd  43125  lptioo2  43126  lptioo1  43127  limcresiooub  43137  limcresioolb  43138  icccncfext  43382  cncfiooicclem1  43388  dvmptfprodlem  43439  stoweidlem34  43529  stoweidlem39  43534  stoweidlem59  43554  stirlinglem8  43576  dirkercncflem2  43599  fourierdlem12  43614  fourierdlem40  43642  fourierdlem42  43644  fourierdlem48  43649  fourierdlem74  43675  fourierdlem75  43676  fourierdlem76  43677  fourierdlem78  43679  fourierdlem93  43694  fourierdlem103  43704  fourierdlem104  43705  elaa2  43729  sge0split  43901  iundjiun  43952  meaiininclem  43978  preimagelt  44190  preimalegt  44191  otiunsndisjX  44722  fun2dmnopgexmpl  44727  0nelsetpreimafv  44794  ichnreuop  44876  0nodd  45316  cznnring  45466