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  5447  pofun  5532  epweon  7657  ord2eln012  8358  disjen  8959  php3  9033  php3OLD  9045  sdom1  9063  sdom1OLD  9064  wemappo  9352  cnfcom2lem  9503  zfregs2  9535  cfsuc  10059  fin1a2lem12  10213  ac6num  10281  canth4  10449  pwfseqlem3  10462  gchpwdom  10472  gchaleph  10473  gchhar  10481  difreicc  13262  fzpreddisj  13351  ccatalpha  14343  s3iunsndisj  14724  fprodntriv  15697  fprodn0f  15746  lcmfunsnlem2lem2  16389  prmreclem5  16666  cidpropd  17464  gsumpropd2lem  18408  isnsgrp  18424  isnmnd  18434  mulgfval  18747  odinf  19215  frgpnabllem1  19519  ablfac1lem  19716  ablsimpgfindlem2  19756  frlmssuvc2  21047  lmmo  22576  xkohaus  22849  snfil  23060  supfil  23091  hauspwpwf1  23183  tsmsfbas  23324  reconnlem2  24035  minveclem3b  24637  dvply1  25489  taylthlem2  25578  wilthlem2  26263  lgseisenlem1  26568  axlowdimlem6  27360  elntg2  27398  structiedg0val  27437  snstriedgval  27453  incistruhgr  27494  umgr2edg1  27623  umgr2edgneu  27626  wlkp1lem1  28086  eupth2eucrct  28626  4cycl2vnunb  28699  frgrncvvdeqlem1  28708  n0lplig  28890  addsqnot2reu  30879  ssmxidllem  31686  qqhf  31981  hgt750lemb  32681  bnj1417  33066  subfacp1lem1  33186  fmlasucdisj  33406  prv0  33437  pocnv  33775  wsuclb  33867  nosepon  33913  filnetlem4  34615  bj-ab0  35137  topdifinffinlem  35562  relowlpssretop  35579  finxpnom  35616  heibor1lem  36011  notornotel2  36298  pmap0  37821  mapdh6eN  39796  mapdh7dN  39806  hdmap1l6e  39870  dvrelogpow2b  40118  aks4d1p1p4  40121  negn0nposznnd  40347  jm2.23  40856  rpnnen3lem  40891  fnwe2lem2  40914  nlimsuc  41086  nlim1NEW  41087  nlim2NEW  41088  nlim3  41089  nlim4  41090  imsqrtvalex  41292  fzdifsuc2  42897  icoiccdif  43111  climrec  43193  sumnnodd  43220  lptioo2  43221  lptioo1  43222  limcresiooub  43232  limcresioolb  43233  icccncfext  43477  cncfiooicclem1  43483  dvmptfprodlem  43534  stoweidlem34  43624  stoweidlem39  43629  stoweidlem59  43649  stirlinglem8  43671  dirkercncflem2  43694  fourierdlem12  43709  fourierdlem40  43737  fourierdlem42  43739  fourierdlem48  43744  fourierdlem74  43770  fourierdlem75  43771  fourierdlem76  43772  fourierdlem78  43774  fourierdlem93  43789  fourierdlem103  43799  fourierdlem104  43800  elaa2  43824  sge0split  43997  iundjiun  44048  meaiininclem  44074  preimagelt  44287  preimalegt  44288  otiunsndisjX  44829  fun2dmnopgexmpl  44834  0nelsetpreimafv  44900  ichnreuop  44982  0nodd  45422  cznnring  45572  et-ltneverrefl  46568