Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylnibr Structured version   Visualization version   GIF version

Theorem sylnibr 318
 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
StepHypRef Expression
1 sylnibr.1 . 2 (𝜑 → ¬ 𝜓)
2 sylnibr.2 . . 3 (𝜒𝜓)
32bicomi 214 . 2 (𝜓𝜒)
41, 3sylnib 317 1 (𝜑 → ¬ 𝜒)
 Colors of variables: wff setvar class 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  5009  pofun  5080  disjen  8158  php3  8187  sdom1  8201  wemappo  8495  cnfcom2lem  8636  zfregs2  8647  cfsuc  9117  fin1a2lem12  9271  ac6num  9339  canth4  9507  pwfseqlem3  9520  gchpwdom  9530  gchaleph  9531  gchhar  9539  difreicc  12342  fzpreddisj  12428  ccatalpha  13411  s3iunsndisj  13753  fprodntriv  14716  fprodn0f  14766  lcmfunsnlem2lem2  15399  prmreclem5  15671  cidpropd  16417  gsumpropd2lem  17320  isnsgrp  17335  isnmnd  17345  odinf  18026  frgpnabllem1  18322  ablfac1lem  18513  frlmssuvc2  20182  lmmo  21232  xkohaus  21504  snfil  21715  supfil  21746  hauspwpwf1  21838  tsmsfbas  21978  reconnlem2  22677  minveclem3b  23245  dvply1  24084  taylthlem2  24173  wilthlem2  24840  lgseisenlem1  25145  axlowdimlem6  25872  structiedg0val  25956  snstriedgval  25975  incistruhgr  26019  umgr2edg1  26148  umgr2edgneu  26151  wlkp1lem1  26626  eupth2eucrct  27195  4cycl2vnunb  27270  frgrncvvdeqlem1  27279  n0lplig  27465  qqhf  30158  signstfvneq0  30777  hgt750lemb  30862  bnj1417  31235  subfacp1lem1  31287  pocnv  31779  wsuclb  31898  nosepon  31943  filnetlem4  32501  bj-ab0  33027  topdifinffinlem  33325  relowlpssretop  33342  finxpnom  33368  heibor1lem  33738  notornotel2  34028  pmap0  35369  mapdh6eN  37346  mapdh7dN  37356  hdmap1l6e  37421  jm2.23  37880  rpnnen3lem  37915  fnwe2lem2  37938  jcn  39519  fzdifsuc2  39838  icoiccdif  40068  climrec  40153  sumnnodd  40180  lptioo2  40181  lptioo1  40182  limcresiooub  40192  limcresioolb  40193  icccncfext  40418  cncfiooicclem1  40424  dvmptfprodlem  40477  stoweidlem34  40569  stoweidlem39  40574  stoweidlem59  40594  stirlinglem8  40616  dirkercncflem2  40639  fourierdlem12  40654  fourierdlem40  40682  fourierdlem42  40684  fourierdlem48  40689  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem78  40719  fourierdlem93  40734  fourierdlem103  40744  fourierdlem104  40745  elaa2  40769  sge0split  40944  iundjiun  40995  meaiininclem  41021  preimagelt  41233  preimalegt  41234  otiunsndisjX  41621  fun2dmnopgexmpl  41626  0nodd  42135  cznnring  42281
 Copyright terms: Public domain W3C validator