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:  otiunsndisj  5501  pofun  5585  epweon  7770  ord2eln012  8478  disjen  9118  php3  9189  sdom1  9206  wemappo  9507  cnfcom2lem  9666  zfregs2  9698  cfsuc  10237  fin1a2lem12  10391  ac6num  10459  canth4  10628  pwfseqlem3  10641  gchpwdom  10651  gchaleph  10652  gchhar  10660  difreicc  13507  fzpreddisj  13597  ccatalpha  14627  s3iunsndisj  15001  fprodntriv  15992  fprodn0f  16041  lcmfunsnlem2lem2  16693  prmreclem5  16976  cidpropd  17762  gsumpropd2lem  18733  isnsgrp  18777  isnmnd  18792  mulgfval  19131  odinf  19629  frgpnabllem1  19939  ablfac1lem  20136  ablsimpgfindlem2  20176  frlmssuvc2  21910  psdmul  22294  lmmo  23502  xkohaus  23775  snfil  23986  supfil  24017  hauspwpwf1  24109  tsmsfbas  24250  reconnlem2  24950  minveclem3b  25552  dvply1  26410  taylthlem2  26499  wilthlem2  27195  lgseisenlem1  27501  nosepon  27791  axlowdimlem6  29234  elntg2  29272  structiedg0val  29309  snstriedgval  29325  incistruhgr  29366  umgr2edg1  29498  umgr2edgneu  29501  wlkp1lem1  29958  eupth2eucrct  30505  4cycl2vnunb  30578  frgrncvvdeqlem1  30587  n0lplig  30772  addsqnot2reu  32769  ssmxidllem  33697  evlextv  33873  esplyindfv  33907  vietalem  33910  fldext2chn  34059  qqhf  34317  hgt750lemb  34984  bnj1417  35370  fineqvnttrclse  35456  subfacp1lem1  35566  fmlasucdisj  35786  prv0  35817  pocnv  36150  wsuclb  36213  filnetlem4  36777  weiunfr  36863  bj-ab0  37428  topdifinffinlem  37876  relowlpssretop  37893  finxpnom  37930  heibor1lem  38343  notornotel2  38630  pmap0  40424  mapdh6eN  42399  mapdh7dN  42409  hdmap1l6e  42473  dvrelogpow2b  42720  aks4d1p1p4  42723  negn0nposznnd  42928  jm2.23  43610  rpnnen3lem  43645  fnwe2lem2  43665  oaordnrex  43909  omnord1ex  43918  oenord1ex  43929  nlimsuc  44054  nlim1NEW  44055  nlim2NEW  44056  nlim3  44057  nlim4  44058  imsqrtvalex  44259  fzdifsuc2  45916  icoiccdif  46127  climrec  46206  sumnnodd  46233  lptioo2  46234  lptioo1  46235  limcresiooub  46243  limcresioolb  46244  icccncfext  46488  cncfiooicclem1  46494  dvmptfprodlem  46545  stoweidlem34  46635  stoweidlem39  46640  stoweidlem59  46660  stirlinglem8  46682  dirkercncflem2  46705  fourierdlem12  46720  fourierdlem40  46748  fourierdlem42  46750  fourierdlem48  46755  fourierdlem74  46781  fourierdlem75  46782  fourierdlem76  46783  fourierdlem78  46785  fourierdlem93  46800  fourierdlem103  46810  fourierdlem104  46811  elaa2  46835  sge0split  47010  iundjiun  47061  meaiininclem  47087  preimagelt  47300  preimalegt  47301  et-ltneverrefl  47472  otiunsndisjX  47900  fun2dmnopgexmpl  47905  0nelsetpreimafv  48023  ichnreuop  48105  gpg3kgrtriexlem5  48736  0nodd  48819  cznnring  48911  smprngprmrng  48988  iineq0  49478