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 223	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	sylnib 328	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  337  otiunsndisj  5521  pofun  5607  epweon  7762  ord2eln012  8497  disjen  9134  php3  9212  php3OLD  9224  sdom1  9242  sdom1OLD  9243  wemappo  9544  cnfcom2lem  9696  zfregs2  9728  cfsuc  10252  fin1a2lem12  10406  ac6num  10474  canth4  10642  pwfseqlem3  10655  gchpwdom  10665  gchaleph  10666  gchhar  10674  difreicc  13461  fzpreddisj  13550  ccatalpha  14543  s3iunsndisj  14915  fprodntriv  15886  fprodn0f  15935  lcmfunsnlem2lem2  16576  prmreclem5  16853  cidpropd  17654  gsumpropd2lem  18598  isnsgrp  18614  isnmnd  18629  mulgfval  18952  odinf  19431  frgpnabllem1  19741  ablfac1lem  19938  ablsimpgfindlem2  19978  frlmssuvc2  21350  lmmo  22884  xkohaus  23157  snfil  23368  supfil  23399  hauspwpwf1  23491  tsmsfbas  23632  reconnlem2  24343  minveclem3b  24945  dvply1  25797  taylthlem2  25886  wilthlem2  26573  lgseisenlem1  26878  nosepon  27168  axlowdimlem6  28205  elntg2  28243  structiedg0val  28282  snstriedgval  28298  incistruhgr  28339  umgr2edg1  28468  umgr2edgneu  28471  wlkp1lem1  28930  eupth2eucrct  29470  4cycl2vnunb  29543  frgrncvvdeqlem1  29552  n0lplig  29736  addsqnot2reu  31726  ssmxidllem  32589  qqhf  32966  hgt750lemb  33668  bnj1417  34052  subfacp1lem1  34170  fmlasucdisj  34390  prv0  34421  pocnv  34733  wsuclb  34800  filnetlem4  35266  bj-ab0  35788  topdifinffinlem  36228  relowlpssretop  36245  finxpnom  36282  heibor1lem  36677  notornotel2  36964  pmap0  38636  mapdh6eN  40611  mapdh7dN  40621  hdmap1l6e  40685  dvrelogpow2b  40933  aks4d1p1p4  40936  negn0nposznnd  41194  jm2.23  41735  rpnnen3lem  41770  fnwe2lem2  41793  oaordnrex  42045  omnord1ex  42054  oenord1ex  42065  nlimsuc  42192  nlim1NEW  42193  nlim2NEW  42194  nlim3  42195  nlim4  42196  imsqrtvalex  42397  fzdifsuc2  44020  icoiccdif  44237  climrec  44319  sumnnodd  44346  lptioo2  44347  lptioo1  44348  limcresiooub  44358  limcresioolb  44359  icccncfext  44603  cncfiooicclem1  44609  dvmptfprodlem  44660  stoweidlem34  44750  stoweidlem39  44755  stoweidlem59  44775  stirlinglem8  44797  dirkercncflem2  44820  fourierdlem12  44835  fourierdlem40  44863  fourierdlem42  44865  fourierdlem48  44870  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem78  44900  fourierdlem93  44915  fourierdlem103  44925  fourierdlem104  44926  elaa2  44950  sge0split  45125  iundjiun  45176  meaiininclem  45202  preimagelt  45415  preimalegt  45416  et-ltneverrefl  45587  otiunsndisjX  45987  fun2dmnopgexmpl  45992  0nelsetpreimafv  46058  ichnreuop  46140  0nodd  46580  cznnring  46854