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  5476  pofun  5558  epweon  7730  ord2eln012  8434  disjen  9074  php3  9145  sdom1  9162  wemappo  9466  cnfcom2lem  9622  zfregs2  9654  cfsuc  10179  fin1a2lem12  10333  ac6num  10401  canth4  10570  pwfseqlem3  10583  gchpwdom  10593  gchaleph  10594  gchhar  10602  difreicc  13412  fzpreddisj  13501  ccatalpha  14529  s3iunsndisj  14903  fprodntriv  15877  fprodn0f  15926  lcmfunsnlem2lem2  16578  prmreclem5  16860  cidpropd  17645  gsumpropd2lem  18616  isnsgrp  18660  isnmnd  18675  mulgfval  19011  odinf  19504  frgpnabllem1  19814  ablfac1lem  20011  ablsimpgfindlem2  20051  frlmssuvc2  21762  psdmul  22121  lmmo  23336  xkohaus  23609  snfil  23820  supfil  23851  hauspwpwf1  23943  tsmsfbas  24084  reconnlem2  24784  minveclem3b  25396  dvply1  26259  taylthlem2  26350  taylthlem2OLD  26351  wilthlem2  27047  lgseisenlem1  27354  nosepon  27645  axlowdimlem6  29032  elntg2  29070  structiedg0val  29107  snstriedgval  29123  incistruhgr  29164  umgr2edg1  29296  umgr2edgneu  29299  wlkp1lem1  29757  eupth2eucrct  30304  4cycl2vnunb  30377  frgrncvvdeqlem1  30386  n0lplig  30571  addsqnot2reu  32572  ssmxidllem  33566  evlextv  33719  esplyindfv  33753  vietalem  33756  fldext2chn  33906  qqhf  34164  hgt750lemb  34834  bnj1417  35217  fineqvnttrclse  35302  subfacp1lem1  35395  fmlasucdisj  35615  prv0  35646  pocnv  35979  wsuclb  36042  filnetlem4  36597  weiunfr  36683  bj-ab0  37156  topdifinffinlem  37602  relowlpssretop  37619  finxpnom  37656  heibor1lem  38060  notornotel2  38347  pmap0  40141  mapdh6eN  42116  mapdh7dN  42126  hdmap1l6e  42190  dvrelogpow2b  42438  aks4d1p1p4  42441  negn0nposznnd  42652  jm2.23  43353  rpnnen3lem  43388  fnwe2lem2  43408  oaordnrex  43652  omnord1ex  43661  oenord1ex  43672  nlimsuc  43797  nlim1NEW  43798  nlim2NEW  43799  nlim3  43800  nlim4  43801  imsqrtvalex  44002  fzdifsuc2  45672  icoiccdif  45884  climrec  45963  sumnnodd  45990  lptioo2  45991  lptioo1  45992  limcresiooub  46000  limcresioolb  46001  icccncfext  46245  cncfiooicclem1  46251  dvmptfprodlem  46302  stoweidlem34  46392  stoweidlem39  46397  stoweidlem59  46417  stirlinglem8  46439  dirkercncflem2  46462  fourierdlem12  46477  fourierdlem40  46505  fourierdlem42  46507  fourierdlem48  46512  fourierdlem74  46538  fourierdlem75  46539  fourierdlem76  46540  fourierdlem78  46542  fourierdlem93  46557  fourierdlem103  46567  fourierdlem104  46568  elaa2  46592  sge0split  46767  iundjiun  46818  meaiininclem  46844  preimagelt  47057  preimalegt  47058  et-ltneverrefl  47229  otiunsndisjX  47639  fun2dmnopgexmpl  47644  0nelsetpreimafv  47750  ichnreuop  47832  gpg3kgrtriexlem5  48447  0nodd  48530  cznnring  48622  iineq0  49179