Theorem sylnibr 330

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

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

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 208

This theorem is referenced by:  otiunsndisj  5461  pofun  5544  epweon  7718  ord2eln012  8422  disjen  9062  php3  9133  sdom1  9150  wemappo  9454  cnfcom2lem  9613  zfregs2  9645  cfsuc  10170  fin1a2lem12  10324  ac6num  10392  canth4  10561  pwfseqlem3  10574  gchpwdom  10584  gchaleph  10585  gchhar  10593  difreicc  13428  fzpreddisj  13518  ccatalpha  14547  s3iunsndisj  14921  fprodntriv  15898  fprodn0f  15947  lcmfunsnlem2lem2  16599  prmreclem5  16882  cidpropd  17667  gsumpropd2lem  18638  isnsgrp  18682  isnmnd  18697  mulgfval  19036  odinf  19529  frgpnabllem1  19839  ablfac1lem  20036  ablsimpgfindlem2  20076  frlmssuvc2  21770  psdmul  22154  lmmo  23363  xkohaus  23636  snfil  23847  supfil  23878  hauspwpwf1  23970  tsmsfbas  24111  reconnlem2  24811  minveclem3b  25413  dvply1  26268  taylthlem2  26357  wilthlem2  27050  lgseisenlem1  27356  nosepon  27647  axlowdimlem6  29034  elntg2  29072  structiedg0val  29109  snstriedgval  29125  incistruhgr  29166  umgr2edg1  29298  umgr2edgneu  29301  wlkp1lem1  29758  eupth2eucrct  30305  4cycl2vnunb  30378  frgrncvvdeqlem1  30387  n0lplig  30572  addsqnot2reu  32573  ssmxidllem  33556  evlextv  33726  esplyindfv  33760  vietalem  33763  fldext2chn  33912  qqhf  34170  hgt750lemb  34840  bnj1417  35223  fineqvnttrclse  35305  subfacp1lem1  35407  fmlasucdisj  35627  prv0  35658  pocnv  35991  wsuclb  36054  filnetlem4  36609  weiunfr  36695  bj-ab0  37261  topdifinffinlem  37709  relowlpssretop  37726  finxpnom  37763  heibor1lem  38176  notornotel2  38463  pmap0  40257  mapdh6eN  42232  mapdh7dN  42242  hdmap1l6e  42306  dvrelogpow2b  42553  aks4d1p1p4  42556  negn0nposznnd  42759  jm2.23  43441  rpnnen3lem  43476  fnwe2lem2  43496  oaordnrex  43740  omnord1ex  43749  oenord1ex  43760  nlimsuc  43885  nlim1NEW  43886  nlim2NEW  43887  nlim3  43888  nlim4  43889  imsqrtvalex  44090  fzdifsuc2  45758  icoiccdif  45969  climrec  46048  sumnnodd  46075  lptioo2  46076  lptioo1  46077  limcresiooub  46085  limcresioolb  46086  icccncfext  46330  cncfiooicclem1  46336  dvmptfprodlem  46387  stoweidlem34  46477  stoweidlem39  46482  stoweidlem59  46502  stirlinglem8  46524  dirkercncflem2  46547  fourierdlem12  46562  fourierdlem40  46590  fourierdlem42  46592  fourierdlem48  46597  fourierdlem74  46623  fourierdlem75  46624  fourierdlem76  46625  fourierdlem78  46627  fourierdlem93  46642  fourierdlem103  46652  fourierdlem104  46653  elaa2  46677  sge0split  46852  iundjiun  46903  meaiininclem  46929  preimagelt  47142  preimalegt  47143  et-ltneverrefl  47314  otiunsndisjX  47742  fun2dmnopgexmpl  47747  0nelsetpreimafv  47865  ichnreuop  47947  gpg3kgrtriexlem5  48578  0nodd  48661  cznnring  48753  iineq0  49310