MPE Home 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  5130  pofun  5203  disjen  8282  php3  8311  sdom1  8325  wemappo  8619  cnfcom2lem  8771  zfregs2  8782  cfsuc  9271  fin1a2lem12  9425  ac6num  9493  canth4  9661  pwfseqlem3  9674  gchpwdom  9684  gchaleph  9685  gchhar  9693  difreicc  12497  fzpreddisj  12583  ccatalpha  13565  s3iunsndisj  13908  fprodntriv  14871  fprodn0f  14921  lcmfunsnlem2lem2  15554  prmreclem5  15826  cidpropd  16571  gsumpropd2lem  17474  isnsgrp  17489  isnmnd  17499  odinf  18180  frgpnabllem1  18476  ablfac1lem  18667  frlmssuvc2  20336  lmmo  21386  xkohaus  21658  snfil  21869  supfil  21900  hauspwpwf1  21992  tsmsfbas  22132  reconnlem2  22831  minveclem3b  23399  dvply1  24238  taylthlem2  24327  wilthlem2  24994  lgseisenlem1  25299  axlowdimlem6  26026  structiedg0val  26110  snstriedgval  26129  incistruhgr  26173  umgr2edg1  26302  umgr2edgneu  26305  wlkp1lem1  26780  eupth2eucrct  27369  4cycl2vnunb  27444  frgrncvvdeqlem1  27453  n0lplig  27646  qqhf  30339  signstfvneq0  30958  hgt750lemb  31043  bnj1417  31416  subfacp1lem1  31468  pocnv  31960  wsuclb  32079  nosepon  32124  filnetlem4  32682  bj-ab0  33208  topdifinffinlem  33506  relowlpssretop  33523  finxpnom  33549  heibor1lem  33921  notornotel2  34211  pmap0  35554  mapdh6eN  37531  mapdh7dN  37541  hdmap1l6e  37606  jm2.23  38065  rpnnen3lem  38100  fnwe2lem2  38123  jcn  39704  fzdifsuc2  40023  icoiccdif  40253  climrec  40338  sumnnodd  40365  lptioo2  40366  lptioo1  40367  limcresiooub  40377  limcresioolb  40378  icccncfext  40603  cncfiooicclem1  40609  dvmptfprodlem  40662  stoweidlem34  40754  stoweidlem39  40759  stoweidlem59  40779  stirlinglem8  40801  dirkercncflem2  40824  fourierdlem12  40839  fourierdlem40  40867  fourierdlem42  40869  fourierdlem48  40874  fourierdlem74  40900  fourierdlem75  40901  fourierdlem76  40902  fourierdlem78  40904  fourierdlem93  40919  fourierdlem103  40929  fourierdlem104  40930  elaa2  40954  sge0split  41129  iundjiun  41180  meaiininclem  41206  preimagelt  41418  preimalegt  41419  otiunsndisjX  41806  fun2dmnopgexmpl  41811  0nodd  42320  cznnring  42466
  Copyright terms: Public domain W3C validator