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

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

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 207

This theorem is referenced by:  otiunsndisj  5524  pofun  5609  epweon  7796  ord2eln012  8536  disjen  9175  php3  9250  php3OLD  9262  sdom1  9279  sdom1OLD  9280  wemappo  9590  cnfcom2lem  9742  zfregs2  9774  cfsuc  10298  fin1a2lem12  10452  ac6num  10520  canth4  10688  pwfseqlem3  10701  gchpwdom  10711  gchaleph  10712  gchhar  10720  difreicc  13525  fzpreddisj  13614  ccatalpha  14632  s3iunsndisj  15008  fprodntriv  15979  fprodn0f  16028  lcmfunsnlem2lem2  16677  prmreclem5  16959  cidpropd  17754  gsumpropd2lem  18693  isnsgrp  18737  isnmnd  18752  mulgfval  19088  odinf  19582  frgpnabllem1  19892  ablfac1lem  20089  ablsimpgfindlem2  20129  frlmssuvc2  21816  psdmul  22171  lmmo  23389  xkohaus  23662  snfil  23873  supfil  23904  hauspwpwf1  23996  tsmsfbas  24137  reconnlem2  24850  minveclem3b  25463  dvply1  26326  taylthlem2  26417  taylthlem2OLD  26418  wilthlem2  27113  lgseisenlem1  27420  nosepon  27711  axlowdimlem6  28963  elntg2  29001  structiedg0val  29040  snstriedgval  29056  incistruhgr  29097  umgr2edg1  29229  umgr2edgneu  29232  wlkp1lem1  29692  eupth2eucrct  30237  4cycl2vnunb  30310  frgrncvvdeqlem1  30319  n0lplig  30503  addsqnot2reu  32506  ssmxidllem  33502  fldext2chn  33770  qqhf  33988  hgt750lemb  34672  bnj1417  35056  subfacp1lem1  35185  fmlasucdisj  35405  prv0  35436  pocnv  35764  wsuclb  35830  filnetlem4  36383  weiunfr  36469  bj-ab0  36910  topdifinffinlem  37349  relowlpssretop  37366  finxpnom  37403  heibor1lem  37817  notornotel2  38104  pmap0  39768  mapdh6eN  41743  mapdh7dN  41753  hdmap1l6e  41817  dvrelogpow2b  42070  aks4d1p1p4  42073  negn0nposznnd  42322  jm2.23  43013  rpnnen3lem  43048  fnwe2lem2  43068  oaordnrex  43313  omnord1ex  43322  oenord1ex  43333  nlimsuc  43459  nlim1NEW  43460  nlim2NEW  43461  nlim3  43462  nlim4  43463  imsqrtvalex  43664  fzdifsuc2  45327  icoiccdif  45542  climrec  45623  sumnnodd  45650  lptioo2  45651  lptioo1  45652  limcresiooub  45662  limcresioolb  45663  icccncfext  45907  cncfiooicclem1  45913  dvmptfprodlem  45964  stoweidlem34  46054  stoweidlem39  46059  stoweidlem59  46079  stirlinglem8  46101  dirkercncflem2  46124  fourierdlem12  46139  fourierdlem40  46167  fourierdlem42  46169  fourierdlem48  46174  fourierdlem74  46200  fourierdlem75  46201  fourierdlem76  46202  fourierdlem78  46204  fourierdlem93  46219  fourierdlem103  46229  fourierdlem104  46230  elaa2  46254  sge0split  46429  iundjiun  46480  meaiininclem  46506  preimagelt  46719  preimalegt  46720  et-ltneverrefl  46891  otiunsndisjX  47296  fun2dmnopgexmpl  47301  0nelsetpreimafv  47382  ichnreuop  47464  gpg3kgrtriexlem5  48048  0nodd  48091  cznnring  48183