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

Theorem sylnib 305
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 301 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  sylnibr  306  ssnelpss  3802  fr3nr  6564  omopthi  7313  inf3lem6  8091  rankxpsuc  8305  cflim2  8644  ssfin4  8691  fin23lem30  8723  isf32lem5  8738  gchhar  9055  qextlt  11447  qextle  11448  fzneuz  11826  vdwnn  14891  psgnunilem3  17080  efgredlemb  17339  gsumzsplit  17503  lspexchn2  18297  lspindp2l  18300  lspindp2  18301  psrlidm  18570  mplcoe1  18632  mplcoe5  18635  evlslem1  18681  ptopn2  20541  regr1lem2  20697  rnelfmlem  20909  hauspwpwf1  20944  tsmssplit  21108  reconn  21788  itg2splitlem  22648  itg2split  22649  itg2cn  22663  wilthlem2  23936  bposlem9  24162  frgra2v  25669  hatomistici  27957  nn0min  28335  2sqcoprm  28359  qqhf  28742  hasheuni  28858  oddpwdc  29139  ballotlemimin  29290  ballotlemfrcn0  29314  ballotlemiminOLD  29328  ballotlemfrcn0OLD  29352  bnj1388  29794  efrunt  30292  dfon2lem4  30383  dfon2lem7  30386  nofulllem5  30544  nandsym1  31031  atbase  32767  llnbase  32986  lplnbase  33011  lvolbase  33055  dalem48  33197  lhpbase  33475  cdlemg17pq  34151  cdlemg19  34163  cdlemg21  34165  dvh3dim3N  34929  rmspecnonsq  35668  setindtr  35792  flcidc  35953  fmul01lt1lem2  37546  icccncfext  37648  stoweidlem14  37757  stoweidlem26  37769  stirlinglem5  37823  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem62  37915  fourierdlem66  37919  hoicvr  38217
  Copyright terms: Public domain W3C validator