Theorem sylnibr 332

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 227	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	sylnib 331	1 ⊢ (𝜑 → ¬ 𝜒)

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

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 210

This theorem is referenced by:  jcndOLD  340  otiunsndisj  5375  pofun  5455  disjen  8658  php3  8687  sdom1  8702  wemappo  8997  cnfcom2lem  9148  zfregs2  9159  cfsuc  9668  fin1a2lem12  9822  ac6num  9890  canth4  10058  pwfseqlem3  10071  gchpwdom  10081  gchaleph  10082  gchhar  10090  difreicc  12862  fzpreddisj  12951  ccatalpha  13938  s3iunsndisj  14319  fprodntriv  15288  fprodn0f  15337  lcmfunsnlem2lem2  15973  prmreclem5  16246  cidpropd  16972  gsumpropd2lem  17881  isnsgrp  17897  isnmnd  17907  mulgfval  18218  odinf  18682  frgpnabllem1  18986  ablfac1lem  19183  ablsimpgfindlem2  19223  frlmssuvc2  20484  lmmo  21985  xkohaus  22258  snfil  22469  supfil  22500  hauspwpwf1  22592  tsmsfbas  22733  reconnlem2  23432  minveclem3b  24032  dvply1  24880  taylthlem2  24969  wilthlem2  25654  lgseisenlem1  25959  axlowdimlem6  26741  elntg2  26779  structiedg0val  26815  snstriedgval  26831  incistruhgr  26872  umgr2edg1  27001  umgr2edgneu  27004  wlkp1lem1  27463  eupth2eucrct  28002  4cycl2vnunb  28075  frgrncvvdeqlem1  28084  n0lplig  28266  addsqnot2reu  30256  ssmxidllem  31049  qqhf  31337  hgt750lemb  32037  bnj1417  32423  subfacp1lem1  32539  fmlasucdisj  32759  prv0  32790  pocnv  33112  wsuclb  33228  nosepon  33285  filnetlem4  33842  bj-ab0  34348  topdifinffinlem  34764  relowlpssretop  34781  finxpnom  34818  heibor1lem  35247  notornotel2  35534  pmap0  37061  mapdh6eN  39036  mapdh7dN  39046  hdmap1l6e  39110  negn0nposznnd  39476  jm2.23  39937  rpnnen3lem  39972  fnwe2lem2  39995  imsqrtvalex  40346  fzdifsuc2  41942  icoiccdif  42161  climrec  42245  sumnnodd  42272  lptioo2  42273  lptioo1  42274  limcresiooub  42284  limcresioolb  42285  icccncfext  42529  cncfiooicclem1  42535  dvmptfprodlem  42586  stoweidlem34  42676  stoweidlem39  42681  stoweidlem59  42701  stirlinglem8  42723  dirkercncflem2  42746  fourierdlem12  42761  fourierdlem40  42789  fourierdlem42  42791  fourierdlem48  42796  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem78  42826  fourierdlem93  42841  fourierdlem103  42851  fourierdlem104  42852  elaa2  42876  sge0split  43048  iundjiun  43099  meaiininclem  43125  preimagelt  43337  preimalegt  43338  otiunsndisjX  43835  fun2dmnopgexmpl  43840  0nelsetpreimafv  43907  ichnreuop  43989  0nodd  44430  cznnring  44580