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

Theorem sylnibr 297
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 194 . 2  |-  ( ps  <->  ch )
41, 3sylnib 296 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  pofun  4479  disjen  7223  php3  7252  sdom1  7267  wemappo  7474  cnfcom2lem  7614  zfregs2  7625  cfsuc  8093  fin1a2lem12  8247  ac6num  8315  canth4  8478  pwfseqlem3  8491  gchhar  8502  gchpwdom  8505  gchaleph  8506  difreicc  10984  prmreclem5  13243  ramcl2lem  13332  cidpropd  13891  odinf  15154  frgpnabllem1  15439  ablfac1lem  15581  lmmo  17398  xkohaus  17638  snfil  17849  supfil  17880  hauspwpwf1  17972  tsmsfbas  18110  reconnlem2  18811  minveclem3b  19282  dvply1  20154  taylthlem2  20243  wilthlem2  20805  perfectlem2  20967  lgseisenlem1  21086  isusgra0  21329  usgra2edg1  21356  nbgra0edg  21397  cusgrares  21434  uvtx01vtx  21454  spthispth  21526  gsumpropd2lem  24173  qqhf  24323  subfacp1lem1  24818  fprodntriv  25221  nofulllem5  25574  axlowdimlem6  25790  filnetlem4  26300  heibor1lem  26408  jm2.23  26957  rpnnen3lem  26992  fnwe2lem2  27016  frlmssuvc2  27115  climrec  27596  stoweidlem34  27650  stoweidlem39  27655  stoweidlem59  27675  stirlinglem8  27697  otiunsndisj  27954  otiunsndisjX  27955  swrd0  28002  frgra2v  28103  4cycl2vnunb  28121  frgrawopreglem4  28150  2spotdisj  28164  2spotiundisj  28165  bnj1417  29116  pmap0  30247  mapdh6eN  32223  mapdh7dN  32233  hdmap1l6e  32298
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 178
  Copyright terms: Public domain W3C validator