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  5474  pofun  5557  epweon  7729  ord2eln012  8432  disjen  9072  php3  9143  sdom1  9160  wemappo  9464  cnfcom2lem  9622  zfregs2  9654  cfsuc  10179  fin1a2lem12  10333  ac6num  10401  canth4  10570  pwfseqlem3  10583  gchpwdom  10593  gchaleph  10594  gchhar  10602  difreicc  13437  fzpreddisj  13527  ccatalpha  14556  s3iunsndisj  14930  fprodntriv  15907  fprodn0f  15956  lcmfunsnlem2lem2  16608  prmreclem5  16891  cidpropd  17676  gsumpropd2lem  18647  isnsgrp  18691  isnmnd  18706  mulgfval  19045  odinf  19538  frgpnabllem1  19848  ablfac1lem  20045  ablsimpgfindlem2  20085  frlmssuvc2  21775  psdmul  22132  lmmo  23345  xkohaus  23618  snfil  23829  supfil  23860  hauspwpwf1  23952  tsmsfbas  24093  reconnlem2  24793  minveclem3b  25395  dvply1  26250  taylthlem2  26339  wilthlem2  27032  lgseisenlem1  27338  nosepon  27629  axlowdimlem6  29016  elntg2  29054  structiedg0val  29091  snstriedgval  29107  incistruhgr  29148  umgr2edg1  29280  umgr2edgneu  29283  wlkp1lem1  29740  eupth2eucrct  30287  4cycl2vnunb  30360  frgrncvvdeqlem1  30369  n0lplig  30554  addsqnot2reu  32555  ssmxidllem  33533  evlextv  33686  esplyindfv  33720  vietalem  33723  fldext2chn  33872  qqhf  34130  hgt750lemb  34800  bnj1417  35183  fineqvnttrclse  35268  subfacp1lem1  35361  fmlasucdisj  35581  prv0  35612  pocnv  35945  wsuclb  36008  filnetlem4  36563  weiunfr  36649  bj-ab0  37215  topdifinffinlem  37663  relowlpssretop  37680  finxpnom  37717  heibor1lem  38130  notornotel2  38417  pmap0  40211  mapdh6eN  42186  mapdh7dN  42196  hdmap1l6e  42260  dvrelogpow2b  42507  aks4d1p1p4  42510  negn0nposznnd  42714  jm2.23  43424  rpnnen3lem  43459  fnwe2lem2  43479  oaordnrex  43723  omnord1ex  43732  oenord1ex  43743  nlimsuc  43868  nlim1NEW  43869  nlim2NEW  43870  nlim3  43871  nlim4  43872  imsqrtvalex  44073  fzdifsuc2  45743  icoiccdif  45954  climrec  46033  sumnnodd  46060  lptioo2  46061  lptioo1  46062  limcresiooub  46070  limcresioolb  46071  icccncfext  46315  cncfiooicclem1  46321  dvmptfprodlem  46372  stoweidlem34  46462  stoweidlem39  46467  stoweidlem59  46487  stirlinglem8  46509  dirkercncflem2  46532  fourierdlem12  46547  fourierdlem40  46575  fourierdlem42  46577  fourierdlem48  46582  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem78  46612  fourierdlem93  46627  fourierdlem103  46637  fourierdlem104  46638  elaa2  46662  sge0split  46837  iundjiun  46888  meaiininclem  46914  preimagelt  47127  preimalegt  47128  et-ltneverrefl  47299  otiunsndisjX  47727  fun2dmnopgexmpl  47732  0nelsetpreimafv  47850  ichnreuop  47932  gpg3kgrtriexlem5  48563  0nodd  48646  cznnring  48738  iineq0  49295