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

Theorem sylnibr 296
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  |-  ( ph  ->  -.  ps )
sylnibr.2  |-  ( ch  <->  ps )
Assertion
Ref Expression
sylnibr  |-  ( ph  ->  -.  ch )

Proof of Theorem sylnibr
StepHypRef Expression
1 sylnibr.1 . 2  |-  ( ph  ->  -.  ps )
2 sylnibr.2 . . 3  |-  ( ch  <->  ps )
32bicomi 193 . 2  |-  ( ps  <->  ch )
41, 3sylnib 295 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  pofun  4367  disjen  7061  php3  7090  sdom1  7105  wemappo  7309  cnfcom2lem  7449  zfregs2  7460  cfsuc  7928  fin1a2lem12  8082  ac6num  8151  canth4  8314  pwfseqlem3  8327  gchhar  8338  gchpwdom  8341  gchaleph  8342  difreicc  10814  prmreclem5  13014  ramcl2lem  13103  cidpropd  13662  odinf  14925  frgpnabllem1  15210  ablfac1lem  15352  lmmo  17164  xkohaus  17403  snfil  17611  supfil  17642  hauspwpwf1  17734  tsmsfbas  17862  reconnlem2  18384  minveclem3b  18845  dvply1  19717  taylthlem2  19806  wilthlem2  20360  perfectlem2  20522  lgseisenlem1  20641  qqhf  23565  subfacp1lem1  23994  fprodntriv  24445  nofulllem5  24745  axlowdimlem6  24961  filnetlem4  25479  heibor1lem  25681  prtlem80  25872  jm2.23  26237  rpnnen3lem  26272  fnwe2lem2  26296  frlmssuvc2  26395  climrec  26877  stoweidlem34  26931  stoweidlem39  26936  stoweidlem59  26956  stirlinglem8  26978  isusgra0  27328  usgra2edg1  27354  nbusgra  27377  nbgra0edg  27381  spthispth  27475  frgra2v  27591  4cycl2vnunb  27609  bnj1417  28582  pmap0  29772  mapdh6eN  31748  mapdh7dN  31758  hdmap1l6e  31823
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator