Theorem sylnibr 331

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

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

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 209

This theorem is referenced by:  otiunsndisj  5483  pofun  5566  epweon  7747  ord2eln012  8454  disjen  9095  php3  9166  sdom1  9183  wemappo  9487  cnfcom2lem  9646  zfregs2  9678  cfsuc  10204  fin1a2lem12  10358  ac6num  10426  canth4  10595  pwfseqlem3  10608  gchpwdom  10618  gchaleph  10619  gchhar  10627  difreicc  13478  fzpreddisj  13568  ccatalpha  14597  s3iunsndisj  14971  fprodntriv  15948  fprodn0f  15997  lcmfunsnlem2lem2  16649  prmreclem5  16932  cidpropd  17718  gsumpropd2lem  18689  isnsgrp  18733  isnmnd  18748  mulgfval  19087  odinf  19579  frgpnabllem1  19889  ablfac1lem  20086  ablsimpgfindlem2  20126  frlmssuvc2  21820  psdmul  22204  lmmo  23413  xkohaus  23686  snfil  23897  supfil  23928  hauspwpwf1  24020  tsmsfbas  24161  reconnlem2  24861  minveclem3b  25463  dvply1  26318  taylthlem2  26407  wilthlem2  27103  lgseisenlem1  27409  nosepon  27699  axlowdimlem6  29087  elntg2  29125  structiedg0val  29162  snstriedgval  29178  incistruhgr  29219  umgr2edg1  29351  umgr2edgneu  29354  wlkp1lem1  29811  eupth2eucrct  30358  4cycl2vnunb  30431  frgrncvvdeqlem1  30440  n0lplig  30625  addsqnot2reu  32626  ssmxidllem  33615  evlextv  33793  esplyindfv  33827  vietalem  33830  fldext2chn  33979  qqhf  34237  hgt750lemb  34907  bnj1417  35293  fineqvnttrclse  35375  subfacp1lem1  35477  fmlasucdisj  35697  prv0  35728  pocnv  36061  wsuclb  36124  filnetlem4  36689  weiunfr  36775  bj-ab0  37341  topdifinffinlem  37789  relowlpssretop  37806  finxpnom  37843  heibor1lem  38256  notornotel2  38543  pmap0  40337  mapdh6eN  42312  mapdh7dN  42322  hdmap1l6e  42386  dvrelogpow2b  42633  aks4d1p1p4  42636  negn0nposznnd  42839  jm2.23  43521  rpnnen3lem  43556  fnwe2lem2  43576  oaordnrex  43820  omnord1ex  43829  oenord1ex  43840  nlimsuc  43965  nlim1NEW  43966  nlim2NEW  43967  nlim3  43968  nlim4  43969  imsqrtvalex  44170  fzdifsuc2  45837  icoiccdif  46048  climrec  46127  sumnnodd  46154  lptioo2  46155  lptioo1  46156  limcresiooub  46164  limcresioolb  46165  icccncfext  46409  cncfiooicclem1  46415  dvmptfprodlem  46466  stoweidlem34  46556  stoweidlem39  46561  stoweidlem59  46581  stirlinglem8  46603  dirkercncflem2  46626  fourierdlem12  46641  fourierdlem40  46669  fourierdlem42  46671  fourierdlem48  46676  fourierdlem74  46702  fourierdlem75  46703  fourierdlem76  46704  fourierdlem78  46706  fourierdlem93  46721  fourierdlem103  46731  fourierdlem104  46732  elaa2  46756  sge0split  46931  iundjiun  46982  meaiininclem  47008  preimagelt  47221  preimalegt  47222  et-ltneverrefl  47393  otiunsndisjX  47821  fun2dmnopgexmpl  47826  0nelsetpreimafv  47944  ichnreuop  48026  gpg3kgrtriexlem5  48657  0nodd  48740  cznnring  48832  iineq0  49389