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

Theorem sylnibr 305
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 202 . 2  |-  ( ps  <->  ch )
41, 3sylnib 304 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184
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 185
This theorem is referenced by:  pofun  4760  disjen  7573  php3  7602  sdom1  7618  wemappo  7869  cnfcom2lem  8040  cnfcom2lemOLD  8048  zfregs2  8059  cfsuc  8532  fin1a2lem12  8686  ac6num  8754  canth4  8920  pwfseqlem3  8933  gchpwdom  8943  gchaleph  8944  gchhar  8952  difreicc  11529  fzpreddisj  11616  lsw0  12380  prmreclem5  14094  ramcl2lem  14183  cidpropd  14763  gsumpropd2lem  15619  odinf  16180  frgpnabllem1  16467  ablfac1lem  16686  frlmssuvc2  18340  frlmssuvc2OLD  18342  lmmo  19111  xkohaus  19353  snfil  19564  supfil  19595  hauspwpwf1  19687  tsmsfbas  19825  reconnlem2  20531  minveclem3b  21042  dvply1  21878  taylthlem2  21967  wilthlem2  22535  perfectlem2  22697  lgseisenlem1  22816  axlowdimlem6  23340  isusgra0  23422  usgra2edg1  23449  nbgra0edg  23490  cusgrares  23527  uvtx01vtx  23547  spthispth  23619  qqhf  26555  signstfvneq0  27112  subfacp1lem1  27206  fprodntriv  27594  wsuclem  27901  wsuclb  27904  nofulllem5  27986  filnetlem4  28745  heibor1lem  28851  jm2.23  29488  rpnnen3lem  29523  fnwe2lem2  29547  climrec  29919  stoweidlem34  29972  stoweidlem39  29977  stoweidlem59  29997  stirlinglem8  30019  otiunsndisj  30275  otiunsndisjX  30276  4cycl2vnunb  30752  frgrawopreglem4  30783  2spotdisj  30797  2spotiundisj  30798  bnj1417  32345  bj-abfal  32722  pmap0  33728  mapdh6eN  35704  mapdh7dN  35714  hdmap1l6e  35779
  Copyright terms: Public domain W3C validator