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

Theorem sylnib 295
Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.)
Hypotheses
Ref Expression
sylnib.1  |-  ( ph  ->  -.  ps )
sylnib.2  |-  ( ps  <->  ch )
Assertion
Ref Expression
sylnib  |-  ( ph  ->  -.  ch )

Proof of Theorem sylnib
StepHypRef Expression
1 sylnib.1 . 2  |-  ( ph  ->  -.  ps )
2 sylnib.2 . . 3  |-  ( ps  <->  ch )
32a1i 10 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
41, 3mtbid 291 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  sylnibr  296  ssnelpss  3517  fr3nr  4571  omopthi  6655  inf3lem6  7334  rankxpsuc  7552  cflim2  7889  ssfin4  7936  fin23lem30  7968  isf32lem5  7983  gchhar  8293  qextlt  10530  qextle  10531  fzneuz  10863  vdwnn  13045  efgredlemb  15055  gsumzsplit  15206  lspexchn2  15884  lspindp2l  15887  lspindp2  15888  psrlidm  16148  mplcoe1  16209  mplcoe2  16211  ptopn2  17279  regr1lem2  17431  rnelfmlem  17647  hauspwpwf1  17682  tsmssplit  17834  reconn  18333  itg2splitlem  19103  itg2split  19104  itg2cn  19118  evlslem1  19399  wilthlem2  20307  bposlem9  20531  hatomistici  22942  ballotlemfrcn0  23088  efrunt  24059  dfon2lem4  24142  dfon2lem7  24145  nofulllem5  24360  nandsym1  24861  bsstrs  26146  nbssntrs  26147  rmspecnonsq  26992  setindtr  27117  flcidc  27379  psgnunilem3  27419  stoweidlem14  27763  stoweidlem26  27775  stirlinglem5  27827  bnj1388  29063  atbase  29479  llnbase  29698  lplnbase  29723  lvolbase  29767  dalem48  29909  lhpbase  30187  cdlemg17pq  30861  cdlemg19  30873  cdlemg21  30875  dvh3dim3N  31639
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