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

Theorem sylnibr 330
 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 225 . 2 (𝜓𝜒)
41, 3sylnib 329 1 (𝜑 → ¬ 𝜒)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207 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 208 This theorem is referenced by:  jcn  338  otiunsndisj  5407  pofun  5490  disjen  8668  php3  8697  sdom1  8712  wemappo  9007  cnfcom2lem  9158  zfregs2  9169  cfsuc  9673  fin1a2lem12  9827  ac6num  9895  canth4  10063  pwfseqlem3  10076  gchpwdom  10086  gchaleph  10087  gchhar  10095  difreicc  12865  fzpreddisj  12951  ccatalpha  13942  s3iunsndisj  14323  fprodntriv  15291  fprodn0f  15340  lcmfunsnlem2lem2  15978  prmreclem5  16251  cidpropd  16975  gsumpropd2lem  17884  isnsgrp  17900  isnmnd  17910  mulgfval  18171  odinf  18626  frgpnabllem1  18929  ablfac1lem  19126  ablsimpgfindlem2  19166  frlmssuvc2  20874  lmmo  21923  xkohaus  22196  snfil  22407  supfil  22438  hauspwpwf1  22530  tsmsfbas  22670  reconnlem2  23369  minveclem3b  23965  dvply1  24807  taylthlem2  24896  wilthlem2  25579  lgseisenlem1  25884  axlowdimlem6  26666  elntg2  26704  structiedg0val  26740  snstriedgval  26756  incistruhgr  26797  umgr2edg1  26926  umgr2edgneu  26929  wlkp1lem1  27388  eupth2eucrct  27929  4cycl2vnunb  28002  frgrncvvdeqlem1  28011  n0lplig  28193  addsqnot2reu  30182  qqhf  31132  hgt750lemb  31832  bnj1417  32216  subfacp1lem1  32329  fmlasucdisj  32549  prv0  32580  pocnv  32902  wsuclb  33018  nosepon  33075  filnetlem4  33632  bj-ab0  34127  topdifinffinlem  34516  relowlpssretop  34533  finxpnom  34570  heibor1lem  34974  notornotel2  35261  pmap0  36787  mapdh6eN  38762  mapdh7dN  38772  hdmap1l6e  38836  negn0nposznnd  39052  jm2.23  39477  rpnnen3lem  39512  fnwe2lem2  39535  fzdifsuc2  41461  icoiccdif  41684  climrec  41768  sumnnodd  41795  lptioo2  41796  lptioo1  41797  limcresiooub  41807  limcresioolb  41808  icccncfext  42054  cncfiooicclem1  42060  dvmptfprodlem  42113  stoweidlem34  42204  stoweidlem39  42209  stoweidlem59  42229  stirlinglem8  42251  dirkercncflem2  42274  fourierdlem12  42289  fourierdlem40  42317  fourierdlem42  42319  fourierdlem48  42324  fourierdlem74  42350  fourierdlem75  42351  fourierdlem76  42352  fourierdlem78  42354  fourierdlem93  42369  fourierdlem103  42379  fourierdlem104  42380  elaa2  42404  sge0split  42576  iundjiun  42627  meaiininclem  42653  preimagelt  42865  preimalegt  42866  otiunsndisjX  43363  fun2dmnopgexmpl  43368  ichnreuop  43485  0nodd  43928  cznnring  44129
 Copyright terms: Public domain W3C validator