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  5503  pofun  5587  epweon  7770  ord2eln012  8478  disjen  9118  php3  9189  sdom1  9206  wemappo  9507  cnfcom2lem  9666  zfregs2  9698  cfsuc  10236  fin1a2lem12  10390  ac6num  10458  canth4  10627  pwfseqlem3  10640  gchpwdom  10650  gchaleph  10651  gchhar  10659  difreicc  13506  fzpreddisj  13597  ccatalpha  14627  s3iunsndisj  15001  fprodntriv  15992  fprodn0f  16041  lcmfunsnlem2lem2  16692  prmreclem5  16975  cidpropd  17761  gsumpropd2lem  18732  isnsgrp  18776  isnmnd  18791  mulgfval  19130  odinf  19628  frgpnabllem1  19938  ablfac1lem  20135  ablsimpgfindlem2  20175  frlmssuvc2  21945  psdmul  22329  lmmo  23537  xkohaus  23810  snfil  24021  supfil  24052  hauspwpwf1  24144  tsmsfbas  24285  reconnlem2  24985  minveclem3b  25587  dvply1  26445  taylthlem2  26537  wilthlem2  27233  lgseisenlem1  27539  nosepon  27829  axlowdimlem6  29297  elntg2  29335  structiedg0val  29372  snstriedgval  29388  incistruhgr  29429  umgr2edg1  29561  umgr2edgneu  29564  wlkp1lem1  30021  eupth2eucrct  30568  4cycl2vnunb  30641  frgrncvvdeqlem1  30650  n0lplig  30835  addsqnot2reu  32832  ssmxidllem  33756  evlextv  33932  esplyindfv  33966  vietalem  33969  fldext2chn  34118  qqhf  34376  hgt750lemb  35043  bnj1417  35429  fineqvnttrclse  35537  subfacp1lem1  35671  fmlasucdisj  35891  prv0  35922  pocnv  36255  wsuclb  36318  filnetlem4  36892  weiunfr  36978  bj-ab0  37543  topdifinffinlem  37993  relowlpssretop  38010  finxpnom  38047  heibor1lem  38460  notornotel2  38745  pmap0  40539  mapdh6eN  42514  mapdh7dN  42524  hdmap1l6e  42588  dvrelogpow2b  42835  aks4d1p1p4  42838  negn0nposznnd  43043  jm2.23  43723  rpnnen3lem  43758  fnwe2lem2  43778  oaordnrex  44022  omnord1ex  44031  oenord1ex  44042  nlimsuc  44167  nlim1NEW  44168  nlim2NEW  44169  nlim3  44170  nlim4  44171  imsqrtvalex  44372  fzdifsuc2  46029  icoiccdif  46240  climrec  46319  sumnnodd  46346  lptioo2  46347  lptioo1  46348  limcresiooub  46356  limcresioolb  46357  icccncfext  46601  cncfiooicclem1  46607  dvmptfprodlem  46658  stoweidlem34  46748  stoweidlem39  46753  stoweidlem59  46773  stirlinglem8  46795  dirkercncflem2  46818  fourierdlem12  46833  fourierdlem40  46861  fourierdlem42  46863  fourierdlem48  46868  fourierdlem74  46894  fourierdlem75  46895  fourierdlem76  46896  fourierdlem78  46898  fourierdlem93  46913  fourierdlem103  46923  fourierdlem104  46924  elaa2  46948  sge0split  47123  iundjiun  47174  meaiininclem  47200  preimagelt  47413  preimalegt  47414  et-ltneverrefl  47585  otiunsndisjX  48016  fun2dmnopgexmpl  48021  0nelsetpreimafv  48139  ichnreuop  48221  gpg3kgrtriexlem5  48852  0nodd  48935  cznnring  49027  smprngprmrng  49104  iineq0  49598