MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylnib Structured version   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  3683  fr3nr  4752  omopthi  6892  inf3lem6  7580  rankxpsuc  7798  cflim2  8135  ssfin4  8182  fin23lem30  8214  isf32lem5  8229  gchhar  8538  qextlt  10781  qextle  10782  fzneuz  11120  vdwnn  13358  efgredlemb  15370  gsumzsplit  15521  lspexchn2  16195  lspindp2l  16198  lspindp2  16199  psrlidm  16459  mplcoe1  16520  mplcoe2  16522  ptopn2  17608  regr1lem2  17764  rnelfmlem  17976  hauspwpwf1  18011  tsmssplit  18173  reconn  18851  itg2splitlem  19632  itg2split  19633  itg2cn  19647  evlslem1  19928  wilthlem2  20844  bposlem9  21068  hatomistici  23857  qqhf  24362  hasheuni  24467  ballotlemimin  24755  ballotlemfrcn0  24779  efrunt  25154  dfon2lem4  25405  dfon2lem7  25408  nofulllem5  25653  nandsym1  26164  rmspecnonsq  26961  setindtr  27086  flcidc  27347  psgnunilem3  27387  fmul01lt1lem2  27682  stoweidlem14  27730  stoweidlem26  27742  stirlinglem5  27794  bnj1388  29339  atbase  30024  llnbase  30243  lplnbase  30268  lvolbase  30312  dalem48  30454  lhpbase  30732  cdlemg17pq  31406  cdlemg19  31418  cdlemg21  31420  dvh3dim3N  32184
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