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  5468  pofun  5550  epweon  7720  ord2eln012  8424  disjen  9062  php3  9133  sdom1  9150  wemappo  9454  cnfcom2lem  9610  zfregs2  9642  cfsuc  10167  fin1a2lem12  10321  ac6num  10389  canth4  10558  pwfseqlem3  10571  gchpwdom  10581  gchaleph  10582  gchhar  10590  difreicc  13400  fzpreddisj  13489  ccatalpha  14517  s3iunsndisj  14891  fprodntriv  15865  fprodn0f  15914  lcmfunsnlem2lem2  16566  prmreclem5  16848  cidpropd  17633  gsumpropd2lem  18604  isnsgrp  18648  isnmnd  18663  mulgfval  18999  odinf  19492  frgpnabllem1  19802  ablfac1lem  19999  ablsimpgfindlem2  20039  frlmssuvc2  21750  psdmul  22109  lmmo  23324  xkohaus  23597  snfil  23808  supfil  23839  hauspwpwf1  23931  tsmsfbas  24072  reconnlem2  24772  minveclem3b  25384  dvply1  26247  taylthlem2  26338  taylthlem2OLD  26339  wilthlem2  27035  lgseisenlem1  27342  nosepon  27633  axlowdimlem6  29020  elntg2  29058  structiedg0val  29095  snstriedgval  29111  incistruhgr  29152  umgr2edg1  29284  umgr2edgneu  29287  wlkp1lem1  29745  eupth2eucrct  30292  4cycl2vnunb  30365  frgrncvvdeqlem1  30374  n0lplig  30558  addsqnot2reu  32560  ssmxidllem  33554  evlextv  33707  esplyindfv  33732  vietalem  33735  fldext2chn  33885  qqhf  34143  hgt750lemb  34813  bnj1417  35197  fineqvnttrclse  35280  subfacp1lem1  35373  fmlasucdisj  35593  prv0  35624  pocnv  35957  wsuclb  36020  filnetlem4  36575  weiunfr  36661  bj-ab0  37109  topdifinffinlem  37552  relowlpssretop  37569  finxpnom  37606  heibor1lem  38010  notornotel2  38297  pmap0  40025  mapdh6eN  42000  mapdh7dN  42010  hdmap1l6e  42074  dvrelogpow2b  42322  aks4d1p1p4  42325  negn0nposznnd  42537  jm2.23  43238  rpnnen3lem  43273  fnwe2lem2  43293  oaordnrex  43537  omnord1ex  43546  oenord1ex  43557  nlimsuc  43682  nlim1NEW  43683  nlim2NEW  43684  nlim3  43685  nlim4  43686  imsqrtvalex  43887  fzdifsuc2  45558  icoiccdif  45770  climrec  45849  sumnnodd  45876  lptioo2  45877  lptioo1  45878  limcresiooub  45886  limcresioolb  45887  icccncfext  46131  cncfiooicclem1  46137  dvmptfprodlem  46188  stoweidlem34  46278  stoweidlem39  46283  stoweidlem59  46303  stirlinglem8  46325  dirkercncflem2  46348  fourierdlem12  46363  fourierdlem40  46391  fourierdlem42  46393  fourierdlem48  46398  fourierdlem74  46424  fourierdlem75  46425  fourierdlem76  46426  fourierdlem78  46428  fourierdlem93  46443  fourierdlem103  46453  fourierdlem104  46454  elaa2  46478  sge0split  46653  iundjiun  46704  meaiininclem  46730  preimagelt  46943  preimalegt  46944  et-ltneverrefl  47115  otiunsndisjX  47525  fun2dmnopgexmpl  47530  0nelsetpreimafv  47636  ichnreuop  47718  gpg3kgrtriexlem5  48333  0nodd  48416  cznnring  48508  iineq0  49065