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  5475  pofun  5557  epweon  7731  ord2eln012  8438  disjen  9075  php3  9150  sdom1  9166  wemappo  9478  cnfcom2lem  9630  zfregs2  9662  cfsuc  10186  fin1a2lem12  10340  ac6num  10408  canth4  10576  pwfseqlem3  10589  gchpwdom  10599  gchaleph  10600  gchhar  10608  difreicc  13421  fzpreddisj  13510  ccatalpha  14534  s3iunsndisj  14910  fprodntriv  15884  fprodn0f  15933  lcmfunsnlem2lem2  16585  prmreclem5  16867  cidpropd  17647  gsumpropd2lem  18582  isnsgrp  18626  isnmnd  18641  mulgfval  18977  odinf  19469  frgpnabllem1  19779  ablfac1lem  19976  ablsimpgfindlem2  20016  frlmssuvc2  21680  psdmul  22029  lmmo  23243  xkohaus  23516  snfil  23727  supfil  23758  hauspwpwf1  23850  tsmsfbas  23991  reconnlem2  24692  minveclem3b  25304  dvply1  26167  taylthlem2  26258  taylthlem2OLD  26259  wilthlem2  26955  lgseisenlem1  27262  nosepon  27553  axlowdimlem6  28850  elntg2  28888  structiedg0val  28925  snstriedgval  28941  incistruhgr  28982  umgr2edg1  29114  umgr2edgneu  29117  wlkp1lem1  29575  eupth2eucrct  30119  4cycl2vnunb  30192  frgrncvvdeqlem1  30201  n0lplig  30385  addsqnot2reu  32388  ssmxidllem  33417  fldext2chn  33691  qqhf  33949  hgt750lemb  34620  bnj1417  35004  subfacp1lem1  35139  fmlasucdisj  35359  prv0  35390  pocnv  35723  wsuclb  35789  filnetlem4  36342  weiunfr  36428  bj-ab0  36869  topdifinffinlem  37308  relowlpssretop  37325  finxpnom  37362  heibor1lem  37776  notornotel2  38063  pmap0  39732  mapdh6eN  41707  mapdh7dN  41717  hdmap1l6e  41781  dvrelogpow2b  42029  aks4d1p1p4  42032  negn0nposznnd  42243  jm2.23  42958  rpnnen3lem  42993  fnwe2lem2  43013  oaordnrex  43257  omnord1ex  43266  oenord1ex  43277  nlimsuc  43403  nlim1NEW  43404  nlim2NEW  43405  nlim3  43406  nlim4  43407  imsqrtvalex  43608  fzdifsuc2  45281  icoiccdif  45495  climrec  45574  sumnnodd  45601  lptioo2  45602  lptioo1  45603  limcresiooub  45613  limcresioolb  45614  icccncfext  45858  cncfiooicclem1  45864  dvmptfprodlem  45915  stoweidlem34  46005  stoweidlem39  46010  stoweidlem59  46030  stirlinglem8  46052  dirkercncflem2  46075  fourierdlem12  46090  fourierdlem40  46118  fourierdlem42  46120  fourierdlem48  46125  fourierdlem74  46151  fourierdlem75  46152  fourierdlem76  46153  fourierdlem78  46155  fourierdlem93  46170  fourierdlem103  46180  fourierdlem104  46181  elaa2  46205  sge0split  46380  iundjiun  46431  meaiininclem  46457  preimagelt  46670  preimalegt  46671  et-ltneverrefl  46842  otiunsndisjX  47253  fun2dmnopgexmpl  47258  0nelsetpreimafv  47364  ichnreuop  47446  gpg3kgrtriexlem5  48051  0nodd  48131  cznnring  48223  iineq0  48781