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 an 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  4330  disjen  7018  php3  7047  sdom1  7062  wemappo  7264  cnfcom2lem  7404  zfregs2  7415  cfsuc  7883  fin1a2lem12  8037  ac6num  8106  canth4  8269  pwfseqlem3  8282  gchhar  8293  gchpwdom  8296  gchaleph  8297  difreicc  10767  prmreclem5  12967  ramcl2lem  13056  cidpropd  13613  odinf  14876  frgpnabllem1  15161  ablfac1lem  15303  lmmo  17108  xkohaus  17347  snfil  17559  supfil  17590  hauspwpwf1  17682  tsmsfbas  17810  reconnlem2  18332  minveclem3b  18792  dvply1  19664  taylthlem2  19753  wilthlem2  20307  perfectlem2  20469  lgseisenlem1  20588  subfacp1lem1  23710  nofulllem5  24360  axlowdimlem6  24575  deref  25288  hpd  26169  filnetlem4  26330  heibor1lem  26533  prtlem80  26724  jm2.23  27089  rpnnen3lem  27124  fnwe2lem2  27148  frlmssuvc2  27247  climrec  27729  stoweidlem34  27783  stoweidlem39  27788  stoweidlem59  27808  stirlinglem8  27830  isusgra0  28106  nbusgra  28143  nbgra0edg  28147  frgra2v  28177  bnj1417  29071  pmap0  29954  mapdh6eN  31930  mapdh7dN  31940  hdmap1l6e  32005
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