Theorem sylnibr 331

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

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

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 209

This theorem is referenced by:  otiunsndisj  5486  pofun  5569  epweon  7753  ord2eln012  8460  disjen  9100  php3  9171  sdom1  9188  wemappo  9491  cnfcom2lem  9650  zfregs2  9682  cfsuc  10208  fin1a2lem12  10362  ac6num  10430  canth4  10599  pwfseqlem3  10612  gchpwdom  10622  gchaleph  10623  gchhar  10631  difreicc  13482  fzpreddisj  13572  ccatalpha  14601  s3iunsndisj  14975  fprodntriv  15963  fprodn0f  16012  lcmfunsnlem2lem2  16664  prmreclem5  16947  cidpropd  17733  gsumpropd2lem  18704  isnsgrp  18748  isnmnd  18763  mulgfval  19102  odinf  19594  frgpnabllem1  19904  ablfac1lem  20101  ablsimpgfindlem2  20141  frlmssuvc2  21835  psdmul  22219  lmmo  23428  xkohaus  23701  snfil  23912  supfil  23943  hauspwpwf1  24035  tsmsfbas  24176  reconnlem2  24876  minveclem3b  25478  dvply1  26336  taylthlem2  26425  wilthlem2  27121  lgseisenlem1  27427  nosepon  27717  axlowdimlem6  29105  elntg2  29143  structiedg0val  29180  snstriedgval  29196  incistruhgr  29237  umgr2edg1  29369  umgr2edgneu  29372  wlkp1lem1  29829  eupth2eucrct  30376  4cycl2vnunb  30449  frgrncvvdeqlem1  30458  n0lplig  30643  addsqnot2reu  32644  ssmxidllem  33622  evlextv  33800  esplyindfv  33834  vietalem  33837  fldext2chn  33986  qqhf  34244  hgt750lemb  34911  bnj1417  35297  fineqvnttrclse  35381  subfacp1lem1  35490  fmlasucdisj  35710  prv0  35741  pocnv  36074  wsuclb  36137  filnetlem4  36702  weiunfr  36788  bj-ab0  37354  topdifinffinlem  37802  relowlpssretop  37819  finxpnom  37856  heibor1lem  38269  notornotel2  38556  pmap0  40350  mapdh6eN  42325  mapdh7dN  42335  hdmap1l6e  42399  dvrelogpow2b  42646  aks4d1p1p4  42649  negn0nposznnd  42852  jm2.23  43534  rpnnen3lem  43569  fnwe2lem2  43589  oaordnrex  43833  omnord1ex  43842  oenord1ex  43853  nlimsuc  43978  nlim1NEW  43979  nlim2NEW  43980  nlim3  43981  nlim4  43982  imsqrtvalex  44183  fzdifsuc2  45850  icoiccdif  46061  climrec  46140  sumnnodd  46167  lptioo2  46168  lptioo1  46169  limcresiooub  46177  limcresioolb  46178  icccncfext  46422  cncfiooicclem1  46428  dvmptfprodlem  46479  stoweidlem34  46569  stoweidlem39  46574  stoweidlem59  46594  stirlinglem8  46616  dirkercncflem2  46639  fourierdlem12  46654  fourierdlem40  46682  fourierdlem42  46684  fourierdlem48  46689  fourierdlem74  46715  fourierdlem75  46716  fourierdlem76  46717  fourierdlem78  46719  fourierdlem93  46734  fourierdlem103  46744  fourierdlem104  46745  elaa2  46769  sge0split  46944  iundjiun  46995  meaiininclem  47021  preimagelt  47234  preimalegt  47235  et-ltneverrefl  47406  otiunsndisjX  47834  fun2dmnopgexmpl  47839  0nelsetpreimafv  47957  ichnreuop  48039  gpg3kgrtriexlem5  48670  0nodd  48753  cznnring  48845  iineq0  49402