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  3890  fr3nr  6600  omopthi  7307  inf3lem6  8051  rankxpsuc  8301  cflim2  8644  ssfin4  8691  fin23lem30  8723  isf32lem5  8738  gchhar  9058  qextlt  11403  qextle  11404  fzneuz  11760  vdwnn  14378  psgnunilem3  16336  efgredlemb  16579  gsumzsplit  16759  gsumzsplitOLD  16760  lspexchn2  17589  lspindp2l  17592  lspindp2  17593  psrlidm  17867  psrlidmOLD  17868  mplcoe1  17938  mplcoe5  17942  mplcoe2OLD  17944  evlslem1  17995  ptopn2  19912  regr1lem2  20068  rnelfmlem  20280  hauspwpwf1  20315  tsmssplit  20481  reconn  21160  itg2splitlem  21982  itg2split  21983  itg2cn  21997  wilthlem2  23168  bposlem9  23392  frgra2v  24772  hatomistici  27054  qqhf  27718  hasheuni  27842  oddpwdc  28044  ballotlemimin  28195  ballotlemfrcn0  28219  efrunt  28836  dfon2lem4  29071  dfon2lem7  29074  nofulllem5  29319  nandsym1  29740  rmspecnonsq  30674  setindtr  30797  flcidc  30955  fmul01lt1lem2  31362  icccncfext  31453  stoweidlem14  31541  stoweidlem26  31553  stirlinglem5  31605  dirkercncflem1  31630  fourierdlem42  31676  fourierdlem66  31700  bnj1388  33385  atbase  34303  llnbase  34522  lplnbase  34547  lvolbase  34591  dalem48  34733  lhpbase  35011  cdlemg17pq  35685  cdlemg19  35697  cdlemg21  35699  dvh3dim3N  36463
  Copyright terms: Public domain W3C validator