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  3530  fr3nr  4587  omopthi  6671  inf3lem6  7350  rankxpsuc  7568  cflim2  7905  ssfin4  7952  fin23lem30  7984  isf32lem5  7999  gchhar  8309  qextlt  10546  qextle  10547  fzneuz  10879  vdwnn  13061  efgredlemb  15071  gsumzsplit  15222  lspexchn2  15900  lspindp2l  15903  lspindp2  15904  psrlidm  16164  mplcoe1  16225  mplcoe2  16227  ptopn2  17295  regr1lem2  17447  rnelfmlem  17663  hauspwpwf1  17698  tsmssplit  17850  reconn  18349  itg2splitlem  19119  itg2split  19120  itg2cn  19134  evlslem1  19415  wilthlem2  20323  bposlem9  20547  hatomistici  22958  ballotlemfrcn0  23104  efrunt  24074  dfon2lem4  24213  dfon2lem7  24216  nofulllem5  24431  nandsym1  24933  bsstrs  26249  nbssntrs  26250  rmspecnonsq  27095  setindtr  27220  flcidc  27482  psgnunilem3  27522  stoweidlem14  27866  stoweidlem26  27878  stirlinglem5  27930  bnj1388  29379  atbase  30101  llnbase  30320  lplnbase  30345  lvolbase  30389  dalem48  30531  lhpbase  30809  cdlemg17pq  31483  cdlemg19  31495  cdlemg21  31497  dvh3dim3N  32261
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