MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylnibr Structured version   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  4519  disjen  7264  php3  7293  sdom1  7308  wemappo  7518  cnfcom2lem  7658  zfregs2  7669  cfsuc  8137  fin1a2lem12  8291  ac6num  8359  canth4  8522  pwfseqlem3  8535  gchhar  8546  gchpwdom  8549  gchaleph  8550  difreicc  11028  prmreclem5  13288  ramcl2lem  13377  cidpropd  13936  odinf  15199  frgpnabllem1  15484  ablfac1lem  15626  lmmo  17444  xkohaus  17685  snfil  17896  supfil  17927  hauspwpwf1  18019  tsmsfbas  18157  reconnlem2  18858  minveclem3b  19329  dvply1  20201  taylthlem2  20290  wilthlem2  20852  perfectlem2  21014  lgseisenlem1  21133  isusgra0  21376  usgra2edg1  21403  nbgra0edg  21444  cusgrares  21481  uvtx01vtx  21501  spthispth  21573  gsumpropd2lem  24220  qqhf  24370  subfacp1lem1  24865  fprodntriv  25268  wsuclem  25576  wsuclb  25579  nofulllem5  25661  axlowdimlem6  25886  filnetlem4  26410  heibor1lem  26518  jm2.23  27067  rpnnen3lem  27102  fnwe2lem2  27126  frlmssuvc2  27224  climrec  27705  stoweidlem34  27759  stoweidlem39  27764  stoweidlem59  27784  stirlinglem8  27806  otiunsndisj  28066  otiunsndisjX  28067  swrd0  28183  lswrd0  28261  frgra2v  28389  4cycl2vnunb  28407  frgrawopreglem4  28436  2spotdisj  28450  2spotiundisj  28451  bnj1417  29410  pmap0  30562  mapdh6eN  32538  mapdh7dN  32548  hdmap1l6e  32613
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