Theorem sylnibr 319

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  otiunsndisj  4980  pofun  5051  disjen  8117  php3  8146  sdom1  8160  wemappo  8454  cnfcom2lem  8598  zfregs2  8609  cfsuc  9079  fin1a2lem12  9233  ac6num  9301  canth4  9469  pwfseqlem3  9482  gchpwdom  9492  gchaleph  9493  gchhar  9501  difreicc  12304  fzpreddisj  12390  ccatalpha  13375  s3iunsndisj  13707  fprodntriv  14672  fprodn0f  14722  lcmfunsnlem2lem2  15352  prmreclem5  15624  cidpropd  16370  gsumpropd2lem  17273  isnsgrp  17288  isnmnd  17298  odinf  17980  frgpnabllem1  18276  ablfac1lem  18467  frlmssuvc2  20134  lmmo  21184  xkohaus  21456  snfil  21668  supfil  21699  hauspwpwf1  21791  tsmsfbas  21931  reconnlem2  22630  minveclem3b  23199  dvply1  24039  taylthlem2  24128  wilthlem2  24795  lgseisenlem1  25100  axlowdimlem6  25827  structiedg0val  25911  snstriedgval  25930  incistruhgr  25974  umgr2edg1  26103  umgr2edgneu  26106  wlkp1lem1  26570  eupth2eucrct  27077  4cycl2vnunb  27154  n0lplig  27335  qqhf  30030  signstfvneq0  30649  hgt750lemb  30734  bnj1417  31109  subfacp1lem1  31161  pocnv  31653  wsuclemOLD  31774  wsuclb  31777  nosepon  31818  filnetlem4  32376  bj-ab0  32902  topdifinffinlem  33195  relowlpssretop  33212  finxpnom  33238  heibor1lem  33608  notornotel2  33898  pmap0  35051  mapdh6eN  37029  mapdh7dN  37039  hdmap1l6e  37104  jm2.23  37563  rpnnen3lem  37598  fnwe2lem2  37621  jcn  39205  fzdifsuc2  39525  icoiccdif  39750  climrec  39835  sumnnodd  39862  lptioo2  39863  lptioo1  39864  limcresiooub  39874  limcresioolb  39875  icccncfext  40100  cncfiooicclem1  40106  dvmptfprodlem  40159  stoweidlem34  40251  stoweidlem39  40256  stoweidlem59  40276  stirlinglem8  40298  dirkercncflem2  40321  fourierdlem12  40336  fourierdlem40  40364  fourierdlem42  40366  fourierdlem48  40371  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem78  40401  fourierdlem93  40416  fourierdlem103  40426  fourierdlem104  40427  elaa2  40451  sge0split  40626  iundjiun  40677  meaiininclem  40700  preimagelt  40912  preimalegt  40913  otiunsndisjX  41298  fun2dmnopgexmpl  41303  0nodd  41810  cznnring  41956