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

Theorem sylnib 304
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 300 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  sylnibr  305  ssnelpss  3763  fr3nr  6412  omopthi  7117  inf3lem6  7860  rankxpsuc  8110  cflim2  8453  ssfin4  8500  fin23lem30  8532  isf32lem5  8547  gchhar  8867  qextlt  11194  qextle  11195  fzneuz  11562  vdwnn  14080  psgnunilem3  16023  efgredlemb  16264  gsumzsplit  16439  gsumzsplitOLD  16440  lspexchn2  17234  lspindp2l  17237  lspindp2  17238  psrlidm  17496  psrlidmOLD  17497  mplcoe1  17566  mplcoe5  17570  mplcoe2OLD  17572  evlslem1  17623  ptopn2  19179  regr1lem2  19335  rnelfmlem  19547  hauspwpwf1  19582  tsmssplit  19748  reconn  20427  itg2splitlem  21248  itg2split  21249  itg2cn  21263  wilthlem2  22429  bposlem9  22653  hatomistici  25788  qqhf  26437  hasheuni  26556  oddpwdc  26759  ballotlemimin  26910  ballotlemfrcn0  26934  efrunt  27386  dfon2lem4  27621  dfon2lem7  27624  nofulllem5  27869  nandsym1  28290  rmspecnonsq  29274  setindtr  29399  flcidc  29557  fmul01lt1lem2  29792  stoweidlem14  29835  stoweidlem26  29847  stirlinglem5  29899  frgra2v  30617  bnj1388  32120  atbase  33030  llnbase  33249  lplnbase  33274  lvolbase  33318  dalem48  33460  lhpbase  33738  cdlemg17pq  34412  cdlemg19  34424  cdlemg21  34426  dvh3dim3N  35190
  Copyright terms: Public domain W3C validator