Theorem sylnibr 318

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

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

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 196

This theorem is referenced by:  otiunsndisj  4905  pofun  4975  disjen  8002  php3  8031  sdom1  8045  wemappo  8337  cnfcom2lem  8481  zfregs2  8492  cfsuc  8962  fin1a2lem12  9116  ac6num  9184  canth4  9348  pwfseqlem3  9361  gchpwdom  9371  gchaleph  9372  gchhar  9380  difreicc  12175  fzpreddisj  12260  ccatalpha  13228  s3iunsndisj  13555  fprodntriv  14511  fprodn0f  14561  lcmfunsnlem2lem2  15190  prmreclem5  15462  cidpropd  16193  gsumpropd2lem  17096  isnsgrp  17111  isnmnd  17121  odinf  17803  frgpnabllem1  18099  ablfac1lem  18290  frlmssuvc2  19953  lmmo  20994  xkohaus  21266  snfil  21478  supfil  21509  hauspwpwf1  21601  tsmsfbas  21741  reconnlem2  22438  minveclem3b  23007  dvply1  23843  taylthlem2  23932  wilthlem2  24595  lgseisenlem1  24900  axlowdimlem6  25627  structiedg0val  25699  snstriedgval  25713  incistruhgr  25746  isusgra0  25876  usgraop  25879  usgra2edg1  25912  nbgra0edg  25961  cusgrares  26001  uvtx01vtx  26020  spthispth  26103  4cycl2vnunb  26544  frgrawopreglem4  26574  2spotdisj  26588  2spotiundisj  26589  qqhf  29358  signstfvneq0  29975  bnj1417  30363  subfacp1lem1  30415  pocnv  30907  wsuclemOLD  31018  wsuclb  31021  nosepon  31066  nofulllem5  31105  filnetlem4  31546  bj-ab0  32094  topdifinffinlem  32371  relowlpssretop  32388  finxpnom  32414  heibor1lem  32778  notornotel2  33068  pmap0  34069  mapdh6eN  36047  mapdh7dN  36057  hdmap1l6e  36122  jm2.23  36581  rpnnen3lem  36616  fnwe2lem2  36639  jcn  38228  fzdifsuc2  38466  icoiccdif  38597  climrec  38670  sumnnodd  38697  lptioo2  38698  lptioo1  38699  limcresiooub  38709  limcresioolb  38710  icccncfext  38773  cncfiooicclem1  38779  dvmptfprodlem  38834  stoweidlem34  38927  stoweidlem39  38932  stoweidlem59  38952  stirlinglem8  38974  dirkercncflem2  38997  fourierdlem12  39012  fourierdlem40  39040  fourierdlem42  39042  fourierdlem48  39047  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem78  39077  fourierdlem93  39092  fourierdlem103  39102  fourierdlem104  39103  elaa2  39127  sge0split  39302  iundjiun  39353  meaiininclem  39376  preimagelt  39589  preimalegt  39590  otiunsndisjX  40317  fun2dmnopgexmpl  40329  umgr2edg1  40438  umgr2edgneu  40441  1wlkp1lem1  40882  eupth2eucrct  41385  4cycl2vnunb-av  41460  frgrwopreglem4  41484  0nodd  41600  cznnring  41748