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

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

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 206

This theorem is referenced by:  otiunsndisj  5516  pofun  5602  epweon  7769  ord2eln012  8509  disjen  9148  php3  9226  php3OLD  9238  sdom1  9256  sdom1OLD  9257  wemappo  9558  cnfcom2lem  9710  zfregs2  9742  cfsuc  10266  fin1a2lem12  10420  ac6num  10488  canth4  10656  pwfseqlem3  10669  gchpwdom  10679  gchaleph  10680  gchhar  10688  difreicc  13479  fzpreddisj  13568  ccatalpha  14561  s3iunsndisj  14933  fprodntriv  15904  fprodn0f  15953  lcmfunsnlem2lem2  16595  prmreclem5  16874  cidpropd  17675  gsumpropd2lem  18624  isnsgrp  18668  isnmnd  18683  mulgfval  19009  odinf  19502  frgpnabllem1  19812  ablfac1lem  20009  ablsimpgfindlem2  20049  frlmssuvc2  21709  lmmo  23258  xkohaus  23531  snfil  23742  supfil  23773  hauspwpwf1  23865  tsmsfbas  24006  reconnlem2  24717  minveclem3b  25330  dvply1  26192  taylthlem2  26283  taylthlem2OLD  26284  wilthlem2  26975  lgseisenlem1  27282  nosepon  27572  axlowdimlem6  28732  elntg2  28770  structiedg0val  28809  snstriedgval  28825  incistruhgr  28866  umgr2edg1  28998  umgr2edgneu  29001  wlkp1lem1  29461  eupth2eucrct  30001  4cycl2vnunb  30074  frgrncvvdeqlem1  30083  n0lplig  30267  addsqnot2reu  32257  ssmxidllem  33109  qqhf  33510  hgt750lemb  34211  bnj1417  34595  subfacp1lem1  34712  fmlasucdisj  34932  prv0  34963  pocnv  35280  wsuclb  35347  filnetlem4  35788  bj-ab0  36309  topdifinffinlem  36749  relowlpssretop  36766  finxpnom  36803  heibor1lem  37204  notornotel2  37491  pmap0  39162  mapdh6eN  41137  mapdh7dN  41147  hdmap1l6e  41211  dvrelogpow2b  41463  aks4d1p1p4  41466  negn0nposznnd  41768  jm2.23  42329  rpnnen3lem  42364  fnwe2lem2  42387  oaordnrex  42637  omnord1ex  42646  oenord1ex  42657  nlimsuc  42784  nlim1NEW  42785  nlim2NEW  42786  nlim3  42787  nlim4  42788  imsqrtvalex  42989  fzdifsuc2  44605  icoiccdif  44822  climrec  44904  sumnnodd  44931  lptioo2  44932  lptioo1  44933  limcresiooub  44943  limcresioolb  44944  icccncfext  45188  cncfiooicclem1  45194  dvmptfprodlem  45245  stoweidlem34  45335  stoweidlem39  45340  stoweidlem59  45360  stirlinglem8  45382  dirkercncflem2  45405  fourierdlem12  45420  fourierdlem40  45448  fourierdlem42  45450  fourierdlem48  45455  fourierdlem74  45481  fourierdlem75  45482  fourierdlem76  45483  fourierdlem78  45485  fourierdlem93  45500  fourierdlem103  45510  fourierdlem104  45511  elaa2  45535  sge0split  45710  iundjiun  45761  meaiininclem  45787  preimagelt  46000  preimalegt  46001  et-ltneverrefl  46172  otiunsndisjX  46572  fun2dmnopgexmpl  46577  0nelsetpreimafv  46643  ichnreuop  46725  0nodd  47145  cznnring  47237