Theorem sylnibr 329

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

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

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 207

This theorem is referenced by:  otiunsndisj  5463  pofun  5545  epweon  7711  ord2eln012  8415  disjen  9051  php3  9123  sdom1  9139  wemappo  9441  cnfcom2lem  9597  zfregs2  9629  cfsuc  10151  fin1a2lem12  10305  ac6num  10373  canth4  10541  pwfseqlem3  10554  gchpwdom  10564  gchaleph  10565  gchhar  10573  difreicc  13387  fzpreddisj  13476  ccatalpha  14500  s3iunsndisj  14875  fprodntriv  15849  fprodn0f  15898  lcmfunsnlem2lem2  16550  prmreclem5  16832  cidpropd  17616  gsumpropd2lem  18553  isnsgrp  18597  isnmnd  18612  mulgfval  18948  odinf  19442  frgpnabllem1  19752  ablfac1lem  19949  ablsimpgfindlem2  19989  frlmssuvc2  21702  psdmul  22051  lmmo  23265  xkohaus  23538  snfil  23749  supfil  23780  hauspwpwf1  23872  tsmsfbas  24013  reconnlem2  24714  minveclem3b  25326  dvply1  26189  taylthlem2  26280  taylthlem2OLD  26281  wilthlem2  26977  lgseisenlem1  27284  nosepon  27575  axlowdimlem6  28892  elntg2  28930  structiedg0val  28967  snstriedgval  28983  incistruhgr  29024  umgr2edg1  29156  umgr2edgneu  29159  wlkp1lem1  29617  eupth2eucrct  30161  4cycl2vnunb  30234  frgrncvvdeqlem1  30243  n0lplig  30427  addsqnot2reu  32430  ssmxidllem  33410  fldext2chn  33695  qqhf  33953  hgt750lemb  34624  bnj1417  35008  subfacp1lem1  35152  fmlasucdisj  35372  prv0  35403  pocnv  35736  wsuclb  35802  filnetlem4  36355  weiunfr  36441  bj-ab0  36882  topdifinffinlem  37321  relowlpssretop  37338  finxpnom  37375  heibor1lem  37789  notornotel2  38076  pmap0  39744  mapdh6eN  41719  mapdh7dN  41729  hdmap1l6e  41793  dvrelogpow2b  42041  aks4d1p1p4  42044  negn0nposznnd  42255  jm2.23  42969  rpnnen3lem  43004  fnwe2lem2  43024  oaordnrex  43268  omnord1ex  43277  oenord1ex  43288  nlimsuc  43414  nlim1NEW  43415  nlim2NEW  43416  nlim3  43417  nlim4  43418  imsqrtvalex  43619  fzdifsuc2  45292  icoiccdif  45505  climrec  45584  sumnnodd  45611  lptioo2  45612  lptioo1  45613  limcresiooub  45623  limcresioolb  45624  icccncfext  45868  cncfiooicclem1  45874  dvmptfprodlem  45925  stoweidlem34  46015  stoweidlem39  46020  stoweidlem59  46040  stirlinglem8  46062  dirkercncflem2  46085  fourierdlem12  46100  fourierdlem40  46128  fourierdlem42  46130  fourierdlem48  46135  fourierdlem74  46161  fourierdlem75  46162  fourierdlem76  46163  fourierdlem78  46165  fourierdlem93  46180  fourierdlem103  46190  fourierdlem104  46191  elaa2  46215  sge0split  46390  iundjiun  46441  meaiininclem  46467  preimagelt  46680  preimalegt  46681  et-ltneverrefl  46852  otiunsndisjX  47263  fun2dmnopgexmpl  47268  0nelsetpreimafv  47374  ichnreuop  47456  gpg3kgrtriexlem5  48071  0nodd  48154  cznnring  48246  iineq0  48804