Theorem sylnibr 328

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 327	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:  jcndOLD  336  otiunsndisj  5520  pofun  5606  epweon  7764  ord2eln012  8499  disjen  9136  php3  9214  php3OLD  9226  sdom1  9244  sdom1OLD  9245  wemappo  9546  cnfcom2lem  9698  zfregs2  9730  cfsuc  10254  fin1a2lem12  10408  ac6num  10476  canth4  10644  pwfseqlem3  10657  gchpwdom  10667  gchaleph  10668  gchhar  10676  difreicc  13463  fzpreddisj  13552  ccatalpha  14545  s3iunsndisj  14917  fprodntriv  15888  fprodn0f  15937  lcmfunsnlem2lem2  16578  prmreclem5  16855  cidpropd  17656  gsumpropd2lem  18600  isnsgrp  18616  isnmnd  18631  mulgfval  18954  odinf  19433  frgpnabllem1  19743  ablfac1lem  19940  ablsimpgfindlem2  19980  frlmssuvc2  21356  lmmo  22891  xkohaus  23164  snfil  23375  supfil  23406  hauspwpwf1  23498  tsmsfbas  23639  reconnlem2  24350  minveclem3b  24952  dvply1  25804  taylthlem2  25893  wilthlem2  26580  lgseisenlem1  26885  nosepon  27175  axlowdimlem6  28243  elntg2  28281  structiedg0val  28320  snstriedgval  28336  incistruhgr  28377  umgr2edg1  28506  umgr2edgneu  28509  wlkp1lem1  28968  eupth2eucrct  29508  4cycl2vnunb  29581  frgrncvvdeqlem1  29590  n0lplig  29774  addsqnot2reu  31764  ssmxidllem  32634  qqhf  33035  hgt750lemb  33737  bnj1417  34121  subfacp1lem1  34239  fmlasucdisj  34459  prv0  34490  pocnv  34802  wsuclb  34869  filnetlem4  35352  bj-ab0  35874  topdifinffinlem  36314  relowlpssretop  36331  finxpnom  36368  heibor1lem  36763  notornotel2  37050  pmap0  38722  mapdh6eN  40697  mapdh7dN  40707  hdmap1l6e  40771  dvrelogpow2b  41019  aks4d1p1p4  41022  negn0nposznnd  41276  jm2.23  41817  rpnnen3lem  41852  fnwe2lem2  41875  oaordnrex  42127  omnord1ex  42136  oenord1ex  42147  nlimsuc  42274  nlim1NEW  42275  nlim2NEW  42276  nlim3  42277  nlim4  42278  imsqrtvalex  42479  fzdifsuc2  44099  icoiccdif  44316  climrec  44398  sumnnodd  44425  lptioo2  44426  lptioo1  44427  limcresiooub  44437  limcresioolb  44438  icccncfext  44682  cncfiooicclem1  44688  dvmptfprodlem  44739  stoweidlem34  44829  stoweidlem39  44834  stoweidlem59  44854  stirlinglem8  44876  dirkercncflem2  44899  fourierdlem12  44914  fourierdlem40  44942  fourierdlem42  44944  fourierdlem48  44949  fourierdlem74  44975  fourierdlem75  44976  fourierdlem76  44977  fourierdlem78  44979  fourierdlem93  44994  fourierdlem103  45004  fourierdlem104  45005  elaa2  45029  sge0split  45204  iundjiun  45255  meaiininclem  45281  preimagelt  45494  preimalegt  45495  et-ltneverrefl  45666  otiunsndisjX  46066  fun2dmnopgexmpl  46071  0nelsetpreimafv  46137  ichnreuop  46219  0nodd  46659  cznnring  46933