Theorem sylnibr 332

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 227	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	sylnib 331	1 ⊢ (𝜑 → ¬ 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  otiunsndisj  5500  pofun  5584  fvtp0  7237  epweon  7821  fnwe2lem3  8184  ord2eln012  8543  disjen  9191  php3  9262  sdom1  9279  wemappo  9580  cnfcom2lem  9739  zfregs2  9771  cfsuc  10374  fin1a2lem12  10528  ac6num  10596  canth4  10771  pwfseqlem3  10784  gchpwdom  10794  gchaleph  10795  gchhar  10803  difreicc  13655  fzpreddisj  13747  ccatalpha  14781  s3iunsndisj  15164  fprodntriv  16153  fprodn0f  16202  lcmfunsnlem2lem2  16858  prmreclem5  17142  cidpropd  17934  gsumpropd2lem  18918  isnsgrp  18962  isnmnd  18977  mulgfval  19329  odinf  19828  frgpnabllem1  20138  ablfac1lem  20335  ablsimpgfindlem2  20375  frlmssuvc2  22156  psdmul  22542  lmmo  23753  xkohaus  24027  snfil  24238  supfil  24269  hauspwpwf1  24361  tsmsfbas  24502  reconnlem2  25202  minveclem3b  25804  dvply1  26660  rnplynfin  26685  taylthlem2  26758  wilthlem2  27453  lgseisenlem1  27759  nosepon  28079  axlowdimlem6  29582  elntg2  29620  structiedg0val  29657  snstriedgval  29673  incistruhgr  29714  umgr2edg1  29849  umgr2edgneu  29852  wlkp1lem1  30309  eupth2eucrct  30875  4cycl2vnunb  30948  frgrncvvdeqlem1  30957  n0lplig  31142  addsqnot2reu  33181  ssmxidllem  34102  evlextv  34285  esplyindfv  34319  vietalem  34322  fldext2chn  34471  qqhf  34729  hgt750lemb  35396  bnj1417  35782  fineqvnttrclse  35933  maxssj0  36047  subfacp1lem1  36152  fmlasucdisj  36372  prv0  36403  pocnv  36743  wsuclb  36805  filnetlem4  37384  weiunfr  37470  bj-ab0  38035  topdifinffinlem  38538  relowlpssretop  38555  finxpnom  38592  heibor1lem  39009  notornotel2  39294  pmap0  41088  mapdh6eN  43063  mapdh7dN  43073  hdmap1l6e  43137  dvrelogpow2b  43384  aks4d1p1p4  43387  negn0nposznnd  43605  jm2.23  44269  rpnnen3lem  44304  oaordnrex  44558  omnord1ex  44567  oenord1ex  44578  nlimsuc  44703  nlim1NEW  44704  nlim2NEW  44705  nlim3  44706  nlim4  44707  imsqrtvalex  44907  fzdifsuc2  46599  icoiccdif  46809  climrec  46888  sumnnodd  46915  lptioo2  46916  lptioo1  46917  limcresiooub  46925  limcresioolb  46926  icccncfext  47170  cncfiooicclem1  47176  dvmptfprodlem  47227  stoweidlem34  47317  stoweidlem39  47322  stoweidlem59  47342  stirlinglem8  47364  dirkercncflem2  47387  fourierdlem12  47402  fourierdlem40  47430  fourierdlem42  47432  fourierdlem48  47437  fourierdlem74  47463  fourierdlem75  47464  fourierdlem76  47465  fourierdlem78  47467  fourierdlem93  47482  fourierdlem103  47492  fourierdlem104  47493  elaa2  47517  sge0split  47692  iundjiun  47743  meaiininclem  47769  preimagelt  47982  preimalegt  47983  et-ltneverrefl  48154  otiunsndisjX  48622  fun2dmnopgexmpl  48627  0nelsetpreimafv  48745  ichnreuop  48827  gpg3kgrtriexlem5  49458  0nodd  49540  cznnring  49632  smprngprmrng  49767  iineq0  50262