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  5539  pofun  5626  epweon  7810  ord2eln012  8553  disjen  9200  php3  9275  php3OLD  9287  sdom1  9305  sdom1OLD  9306  wemappo  9618  cnfcom2lem  9770  zfregs2  9802  cfsuc  10326  fin1a2lem12  10480  ac6num  10548  canth4  10716  pwfseqlem3  10729  gchpwdom  10739  gchaleph  10740  gchhar  10748  difreicc  13544  fzpreddisj  13633  ccatalpha  14641  s3iunsndisj  15017  fprodntriv  15990  fprodn0f  16039  lcmfunsnlem2lem2  16686  prmreclem5  16967  cidpropd  17768  gsumpropd2lem  18717  isnsgrp  18761  isnmnd  18776  mulgfval  19109  odinf  19605  frgpnabllem1  19915  ablfac1lem  20112  ablsimpgfindlem2  20152  frlmssuvc2  21838  psdmul  22193  lmmo  23409  xkohaus  23682  snfil  23893  supfil  23924  hauspwpwf1  24016  tsmsfbas  24157  reconnlem2  24868  minveclem3b  25481  dvply1  26343  taylthlem2  26434  taylthlem2OLD  26435  wilthlem2  27130  lgseisenlem1  27437  nosepon  27728  axlowdimlem6  28980  elntg2  29018  structiedg0val  29057  snstriedgval  29073  incistruhgr  29114  umgr2edg1  29246  umgr2edgneu  29249  wlkp1lem1  29709  eupth2eucrct  30249  4cycl2vnunb  30322  frgrncvvdeqlem1  30331  n0lplig  30515  addsqnot2reu  32514  ssmxidllem  33466  fldext2chn  33719  qqhf  33932  hgt750lemb  34633  bnj1417  35017  subfacp1lem1  35147  fmlasucdisj  35367  prv0  35398  pocnv  35725  wsuclb  35792  filnetlem4  36347  weiunfr  36433  bj-ab0  36874  topdifinffinlem  37313  relowlpssretop  37330  finxpnom  37367  heibor1lem  37769  notornotel2  38056  pmap0  39722  mapdh6eN  41697  mapdh7dN  41707  hdmap1l6e  41771  dvrelogpow2b  42025  aks4d1p1p4  42028  negn0nposznnd  42271  jm2.23  42953  rpnnen3lem  42988  fnwe2lem2  43008  oaordnrex  43257  omnord1ex  43266  oenord1ex  43277  nlimsuc  43403  nlim1NEW  43404  nlim2NEW  43405  nlim3  43406  nlim4  43407  imsqrtvalex  43608  fzdifsuc2  45225  icoiccdif  45442  climrec  45524  sumnnodd  45551  lptioo2  45552  lptioo1  45553  limcresiooub  45563  limcresioolb  45564  icccncfext  45808  cncfiooicclem1  45814  dvmptfprodlem  45865  stoweidlem34  45955  stoweidlem39  45960  stoweidlem59  45980  stirlinglem8  46002  dirkercncflem2  46025  fourierdlem12  46040  fourierdlem40  46068  fourierdlem42  46070  fourierdlem48  46075  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem78  46105  fourierdlem93  46120  fourierdlem103  46130  fourierdlem104  46131  elaa2  46155  sge0split  46330  iundjiun  46381  meaiininclem  46407  preimagelt  46620  preimalegt  46621  et-ltneverrefl  46792  otiunsndisjX  47194  fun2dmnopgexmpl  47199  0nelsetpreimafv  47264  ichnreuop  47346  0nodd  47893  cznnring  47985