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  3730  fr3nr  6380  omopthi  7084  inf3lem6  7827  rankxpsuc  8077  cflim2  8420  ssfin4  8467  fin23lem30  8499  isf32lem5  8514  gchhar  8833  qextlt  11160  qextle  11161  fzneuz  11524  vdwnn  14041  psgnunilem3  15981  efgredlemb  16222  gsumzsplit  16397  gsumzsplitOLD  16398  lspexchn2  17133  lspindp2l  17136  lspindp2  17137  psrlidm  17407  psrlidmOLD  17408  mplcoe1  17477  mplcoe2  17480  mplcoe2OLD  17481  ptopn2  18998  regr1lem2  19154  rnelfmlem  19366  hauspwpwf1  19401  tsmssplit  19567  reconn  20246  itg2splitlem  21067  itg2split  21068  itg2cn  21082  evlslem1  21366  wilthlem2  22291  bposlem9  22515  hatomistici  25588  qqhf  26268  hasheuni  26387  oddpwdc  26584  ballotlemimin  26735  ballotlemfrcn0  26759  efrunt  27210  dfon2lem4  27445  dfon2lem7  27448  nofulllem5  27693  nandsym1  28115  rmspecnonsq  29090  setindtr  29215  flcidc  29373  fmul01lt1lem2  29608  stoweidlem14  29652  stoweidlem26  29664  stirlinglem5  29716  frgra2v  30434  bnj1388  31723  atbase  32504  llnbase  32723  lplnbase  32748  lvolbase  32792  dalem48  32934  lhpbase  33212  cdlemg17pq  33886  cdlemg19  33898  cdlemg21  33900  dvh3dim3N  34664
  Copyright terms: Public domain W3C validator