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  3634  fr3nr  4700  omopthi  6836  inf3lem6  7521  rankxpsuc  7739  cflim2  8076  ssfin4  8123  fin23lem30  8155  isf32lem5  8170  gchhar  8479  qextlt  10721  qextle  10722  fzneuz  11058  vdwnn  13293  efgredlemb  15305  gsumzsplit  15456  lspexchn2  16130  lspindp2l  16133  lspindp2  16134  psrlidm  16394  mplcoe1  16455  mplcoe2  16457  ptopn2  17537  regr1lem2  17693  rnelfmlem  17905  hauspwpwf1  17940  tsmssplit  18102  reconn  18730  itg2splitlem  19507  itg2split  19508  itg2cn  19522  evlslem1  19803  wilthlem2  20719  bposlem9  20943  hatomistici  23713  qqhf  24169  hasheuni  24271  ballotlemimin  24542  ballotlemfrcn0  24566  efrunt  24941  dfon2lem4  25166  dfon2lem7  25169  nofulllem5  25384  nandsym1  25886  rmspecnonsq  26661  setindtr  26786  flcidc  27048  psgnunilem3  27088  fmul01lt1lem2  27383  stoweidlem14  27431  stoweidlem26  27443  stirlinglem5  27495  bnj1388  28740  atbase  29404  llnbase  29623  lplnbase  29648  lvolbase  29692  dalem48  29834  lhpbase  30112  cdlemg17pq  30786  cdlemg19  30798  cdlemg21  30800  dvh3dim3N  31564
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