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  5465  pofun  5547  epweon  7717  ord2eln012  8421  disjen  9058  php3  9129  sdom1  9145  wemappo  9446  cnfcom2lem  9602  zfregs2  9634  cfsuc  10159  fin1a2lem12  10313  ac6num  10381  canth4  10549  pwfseqlem3  10562  gchpwdom  10572  gchaleph  10573  gchhar  10581  difreicc  13391  fzpreddisj  13480  ccatalpha  14508  s3iunsndisj  14882  fprodntriv  15856  fprodn0f  15905  lcmfunsnlem2lem2  16557  prmreclem5  16839  cidpropd  17624  gsumpropd2lem  18595  isnsgrp  18639  isnmnd  18654  mulgfval  18990  odinf  19483  frgpnabllem1  19793  ablfac1lem  19990  ablsimpgfindlem2  20030  frlmssuvc2  21741  psdmul  22100  lmmo  23315  xkohaus  23588  snfil  23799  supfil  23830  hauspwpwf1  23922  tsmsfbas  24063  reconnlem2  24763  minveclem3b  25375  dvply1  26238  taylthlem2  26329  taylthlem2OLD  26330  wilthlem2  27026  lgseisenlem1  27333  nosepon  27624  axlowdimlem6  28946  elntg2  28984  structiedg0val  29021  snstriedgval  29037  incistruhgr  29078  umgr2edg1  29210  umgr2edgneu  29213  wlkp1lem1  29671  eupth2eucrct  30218  4cycl2vnunb  30291  frgrncvvdeqlem1  30300  n0lplig  30484  addsqnot2reu  32486  ssmxidllem  33482  evlextv  33635  esplyindfv  33660  vietalem  33663  fldext2chn  33813  qqhf  34071  hgt750lemb  34741  bnj1417  35125  fineqvnttrclse  35216  subfacp1lem1  35295  fmlasucdisj  35515  prv0  35546  pocnv  35879  wsuclb  35942  filnetlem4  36497  weiunfr  36583  bj-ab0  37025  topdifinffinlem  37464  relowlpssretop  37481  finxpnom  37518  heibor1lem  37922  notornotel2  38209  pmap0  39937  mapdh6eN  41912  mapdh7dN  41922  hdmap1l6e  41986  dvrelogpow2b  42234  aks4d1p1p4  42237  negn0nposznnd  42452  jm2.23  43153  rpnnen3lem  43188  fnwe2lem2  43208  oaordnrex  43452  omnord1ex  43461  oenord1ex  43472  nlimsuc  43598  nlim1NEW  43599  nlim2NEW  43600  nlim3  43601  nlim4  43602  imsqrtvalex  43803  fzdifsuc2  45474  icoiccdif  45686  climrec  45765  sumnnodd  45792  lptioo2  45793  lptioo1  45794  limcresiooub  45802  limcresioolb  45803  icccncfext  46047  cncfiooicclem1  46053  dvmptfprodlem  46104  stoweidlem34  46194  stoweidlem39  46199  stoweidlem59  46219  stirlinglem8  46241  dirkercncflem2  46264  fourierdlem12  46279  fourierdlem40  46307  fourierdlem42  46309  fourierdlem48  46314  fourierdlem74  46340  fourierdlem75  46341  fourierdlem76  46342  fourierdlem78  46344  fourierdlem93  46359  fourierdlem103  46369  fourierdlem104  46370  elaa2  46394  sge0split  46569  iundjiun  46620  meaiininclem  46646  preimagelt  46859  preimalegt  46860  et-ltneverrefl  47031  otiunsndisjX  47441  fun2dmnopgexmpl  47446  0nelsetpreimafv  47552  ichnreuop  47634  gpg3kgrtriexlem5  48249  0nodd  48332  cznnring  48424  iineq0  48981