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  5530  pofun  5615  epweon  7794  ord2eln012  8534  disjen  9173  php3  9247  php3OLD  9259  sdom1  9276  sdom1OLD  9277  wemappo  9587  cnfcom2lem  9739  zfregs2  9771  cfsuc  10295  fin1a2lem12  10449  ac6num  10517  canth4  10685  pwfseqlem3  10698  gchpwdom  10708  gchaleph  10709  gchhar  10717  difreicc  13521  fzpreddisj  13610  ccatalpha  14628  s3iunsndisj  15004  fprodntriv  15975  fprodn0f  16024  lcmfunsnlem2lem2  16673  prmreclem5  16954  cidpropd  17755  gsumpropd2lem  18705  isnsgrp  18749  isnmnd  18764  mulgfval  19100  odinf  19596  frgpnabllem1  19906  ablfac1lem  20103  ablsimpgfindlem2  20143  frlmssuvc2  21833  psdmul  22188  lmmo  23404  xkohaus  23677  snfil  23888  supfil  23919  hauspwpwf1  24011  tsmsfbas  24152  reconnlem2  24863  minveclem3b  25476  dvply1  26340  taylthlem2  26431  taylthlem2OLD  26432  wilthlem2  27127  lgseisenlem1  27434  nosepon  27725  axlowdimlem6  28977  elntg2  29015  structiedg0val  29054  snstriedgval  29070  incistruhgr  29111  umgr2edg1  29243  umgr2edgneu  29246  wlkp1lem1  29706  eupth2eucrct  30246  4cycl2vnunb  30319  frgrncvvdeqlem1  30328  n0lplig  30512  addsqnot2reu  32514  ssmxidllem  33481  fldext2chn  33734  qqhf  33949  hgt750lemb  34650  bnj1417  35034  subfacp1lem1  35164  fmlasucdisj  35384  prv0  35415  pocnv  35743  wsuclb  35810  filnetlem4  36364  weiunfr  36450  bj-ab0  36891  topdifinffinlem  37330  relowlpssretop  37347  finxpnom  37384  heibor1lem  37796  notornotel2  38083  pmap0  39748  mapdh6eN  41723  mapdh7dN  41733  hdmap1l6e  41797  dvrelogpow2b  42050  aks4d1p1p4  42053  negn0nposznnd  42296  jm2.23  42985  rpnnen3lem  43020  fnwe2lem2  43040  oaordnrex  43285  omnord1ex  43294  oenord1ex  43305  nlimsuc  43431  nlim1NEW  43432  nlim2NEW  43433  nlim3  43434  nlim4  43435  imsqrtvalex  43636  fzdifsuc2  45261  icoiccdif  45477  climrec  45559  sumnnodd  45586  lptioo2  45587  lptioo1  45588  limcresiooub  45598  limcresioolb  45599  icccncfext  45843  cncfiooicclem1  45849  dvmptfprodlem  45900  stoweidlem34  45990  stoweidlem39  45995  stoweidlem59  46015  stirlinglem8  46037  dirkercncflem2  46060  fourierdlem12  46075  fourierdlem40  46103  fourierdlem42  46105  fourierdlem48  46110  fourierdlem74  46136  fourierdlem75  46137  fourierdlem76  46138  fourierdlem78  46140  fourierdlem93  46155  fourierdlem103  46165  fourierdlem104  46166  elaa2  46190  sge0split  46365  iundjiun  46416  meaiininclem  46442  preimagelt  46655  preimalegt  46656  et-ltneverrefl  46827  otiunsndisjX  47229  fun2dmnopgexmpl  47234  0nelsetpreimafv  47315  ichnreuop  47397  0nodd  48014  cznnring  48106