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

Theorem sylnib 296
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 11 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
41, 3mtbid 292 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  sylnibr  297  ssnelpss  3651  fr3nr  4719  omopthi  6859  inf3lem6  7544  rankxpsuc  7762  cflim2  8099  ssfin4  8146  fin23lem30  8178  isf32lem5  8193  gchhar  8502  qextlt  10745  qextle  10746  fzneuz  11083  vdwnn  13321  efgredlemb  15333  gsumzsplit  15484  lspexchn2  16158  lspindp2l  16161  lspindp2  16162  psrlidm  16422  mplcoe1  16483  mplcoe2  16485  ptopn2  17569  regr1lem2  17725  rnelfmlem  17937  hauspwpwf1  17972  tsmssplit  18134  reconn  18812  itg2splitlem  19593  itg2split  19594  itg2cn  19608  evlslem1  19889  wilthlem2  20805  bposlem9  21029  hatomistici  23818  qqhf  24323  hasheuni  24428  ballotlemimin  24716  ballotlemfrcn0  24740  efrunt  25115  dfon2lem4  25356  dfon2lem7  25359  nofulllem5  25574  nandsym1  26076  rmspecnonsq  26860  setindtr  26985  flcidc  27247  psgnunilem3  27287  fmul01lt1lem2  27582  stoweidlem14  27630  stoweidlem26  27642  stirlinglem5  27694  bnj1388  29108  atbase  29772  llnbase  29991  lplnbase  30016  lvolbase  30060  dalem48  30202  lhpbase  30480  cdlemg17pq  31154  cdlemg19  31166  cdlemg21  31168  dvh3dim3N  31932
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