Theorem sylnibr 332

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

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

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 210

This theorem is referenced by:  jcndOLD  340  otiunsndisj  5377  pofun  5460  disjen  8724  php3  8753  sdom1  8797  wemappo  9086  cnfcom2lem  9237  zfregs2  9248  cfsuc  9757  fin1a2lem12  9911  ac6num  9979  canth4  10147  pwfseqlem3  10160  gchpwdom  10170  gchaleph  10171  gchhar  10179  difreicc  12958  fzpreddisj  13047  ccatalpha  14036  s3iunsndisj  14417  fprodntriv  15388  fprodn0f  15437  lcmfunsnlem2lem2  16080  prmreclem5  16356  cidpropd  17084  gsumpropd2lem  18005  isnsgrp  18021  isnmnd  18031  mulgfval  18344  odinf  18808  frgpnabllem1  19112  ablfac1lem  19309  ablsimpgfindlem2  19349  frlmssuvc2  20611  lmmo  22131  xkohaus  22404  snfil  22615  supfil  22646  hauspwpwf1  22738  tsmsfbas  22879  reconnlem2  23579  minveclem3b  24180  dvply1  25032  taylthlem2  25121  wilthlem2  25806  lgseisenlem1  26111  axlowdimlem6  26893  elntg2  26931  structiedg0val  26967  snstriedgval  26983  incistruhgr  27024  umgr2edg1  27153  umgr2edgneu  27156  wlkp1lem1  27615  eupth2eucrct  28154  4cycl2vnunb  28227  frgrncvvdeqlem1  28236  n0lplig  28418  addsqnot2reu  30408  ssmxidllem  31213  qqhf  31506  hgt750lemb  32206  bnj1417  32592  subfacp1lem1  32712  fmlasucdisj  32932  prv0  32963  pocnv  33302  wsuclb  33433  nosepon  33509  filnetlem4  34208  bj-ab0  34725  topdifinffinlem  35141  relowlpssretop  35158  finxpnom  35195  heibor1lem  35590  notornotel2  35877  pmap0  37402  mapdh6eN  39377  mapdh7dN  39387  hdmap1l6e  39451  dvrelogpow2b  39695  aks4d1p1p4  39698  negn0nposznnd  39886  jm2.23  40390  rpnnen3lem  40425  fnwe2lem2  40448  imsqrtvalex  40799  fzdifsuc2  42387  icoiccdif  42602  climrec  42686  sumnnodd  42713  lptioo2  42714  lptioo1  42715  limcresiooub  42725  limcresioolb  42726  icccncfext  42970  cncfiooicclem1  42976  dvmptfprodlem  43027  stoweidlem34  43117  stoweidlem39  43122  stoweidlem59  43142  stirlinglem8  43164  dirkercncflem2  43187  fourierdlem12  43202  fourierdlem40  43230  fourierdlem42  43232  fourierdlem48  43237  fourierdlem74  43263  fourierdlem75  43264  fourierdlem76  43265  fourierdlem78  43267  fourierdlem93  43282  fourierdlem103  43292  fourierdlem104  43293  elaa2  43317  sge0split  43489  iundjiun  43540  meaiininclem  43566  preimagelt  43778  preimalegt  43779  otiunsndisjX  44304  fun2dmnopgexmpl  44309  0nelsetpreimafv  44376  ichnreuop  44458  0nodd  44898  cznnring  45048