MPE Home 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  5401  pofun  5484  disjen  8662  php3  8691  sdom1  8706  wemappo  9001  cnfcom2lem  9152  zfregs2  9163  cfsuc  9667  fin1a2lem12  9821  ac6num  9889  canth4  10057  pwfseqlem3  10070  gchpwdom  10080  gchaleph  10081  gchhar  10089  difreicc  12858  fzpreddisj  12944  ccatalpha  13935  s3iunsndisj  14316  fprodntriv  15284  fprodn0f  15333  lcmfunsnlem2lem2  15971  prmreclem5  16244  cidpropd  16968  gsumpropd2lem  17877  isnsgrp  17893  isnmnd  17903  mulgfval  18164  odinf  18619  frgpnabllem1  18922  ablfac1lem  19119  ablsimpgfindlem2  19159  frlmssuvc2  20867  lmmo  21916  xkohaus  22189  snfil  22400  supfil  22431  hauspwpwf1  22523  tsmsfbas  22663  reconnlem2  23362  minveclem3b  23958  dvply1  24800  taylthlem2  24889  wilthlem2  25573  lgseisenlem1  25878  axlowdimlem6  26660  elntg2  26698  structiedg0val  26734  snstriedgval  26750  incistruhgr  26791  umgr2edg1  26920  umgr2edgneu  26923  wlkp1lem1  27382  eupth2eucrct  27923  4cycl2vnunb  27996  frgrncvvdeqlem1  28005  n0lplig  28187  addsqnot2reu  30176  qqhf  31126  hgt750lemb  31826  bnj1417  32210  subfacp1lem1  32323  fmlasucdisj  32543  prv0  32574  pocnv  32896  wsuclb  33012  nosepon  33069  filnetlem4  33626  bj-ab0  34121  topdifinffinlem  34510  relowlpssretop  34527  finxpnom  34564  heibor1lem  34968  notornotel2  35255  pmap0  36781  mapdh6eN  38756  mapdh7dN  38766  hdmap1l6e  38830  negn0nposznnd  39046  jm2.23  39471  rpnnen3lem  39506  fnwe2lem2  39529  fzdifsuc2  41453  icoiccdif  41676  climrec  41760  sumnnodd  41787  lptioo2  41788  lptioo1  41789  limcresiooub  41799  limcresioolb  41800  icccncfext  42046  cncfiooicclem1  42052  dvmptfprodlem  42105  stoweidlem34  42196  stoweidlem39  42201  stoweidlem59  42221  stirlinglem8  42243  dirkercncflem2  42266  fourierdlem12  42281  fourierdlem40  42309  fourierdlem42  42311  fourierdlem48  42316  fourierdlem74  42342  fourierdlem75  42343  fourierdlem76  42344  fourierdlem78  42346  fourierdlem93  42361  fourierdlem103  42371  fourierdlem104  42372  elaa2  42396  sge0split  42568  iundjiun  42619  meaiininclem  42645  preimagelt  42857  preimalegt  42858  otiunsndisjX  43355  fun2dmnopgexmpl  43360  0nelsetpreimafv  43427  ichnreuop  43511  0nodd  43954  cznnring  44155
  Copyright terms: Public domain W3C validator