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

Theorem nsyl 116
Description: A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
Hypotheses
Ref Expression
nsyl.1  |-  ( ph  ->  -.  ps )
nsyl.2  |-  ( ch 
->  ps )
Assertion
Ref Expression
nsyl  |-  ( ph  ->  -.  ch )

Proof of Theorem nsyl
StepHypRef Expression
1 nsyl.1 . . 3  |-  ( ph  ->  -.  ps )
2 nsyl.2 . . 3  |-  ( ch 
->  ps )
31, 2nsyl3 114 . 2  |-  ( ch 
->  -.  ph )
43con2i 115 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  con3i  130  intnand  884  intnanrd  885  intn3an1d  1294  intn3an2d  1295  intn3an3d  1296  ax12OLD  2021  ax6  2226  ax12from12o  2235  camestres  2387  camestros  2391  calemes  2398  calemos  2401  pssn2lp  3450  sotrieq  4532  ordnbtwn  4674  dfwe2  4764  funun  5497  canth  6541  pwuninel2  6546  swoer  6935  swoord1  6936  swoord2  6937  php2  7294  cantnfp1lem1  7636  cantnfp1lem3  7638  cantnflem2  7648  en3lp  7674  rankxpsuc  7808  cardmin2  7887  infxpenlem  7897  cardaleph  7972  isfin4-3  8197  fin23lem24  8204  fin23lem25  8206  fin23lem26  8207  fin23lem38  8231  isfin32i  8247  fin34  8272  fin67  8277  nd3  8466  fpwwe2lem13  8519  canthnum  8526  canthwe  8528  pwfseq  8541  gchcdaidm  8545  gchxpidm  8546  winainflem  8570  r1wunlim  8614  suplem2pr  8932  elnnz  10294  fzneuz  11130  fzodisj  11169  hasheq0  11646  cnpart  12047  sqreulem  12165  rlimuni  12346  rlimcld2  12374  divalglem6  12920  bitsf1  12960  infpnlem1  13280  ramubcl  13388  ressress  13528  mreexmrid  13870  gsum2d  15548  ablfacrplem  15625  mplsubrglem  16504  infil  17897  fbasfip  17902  fgcl  17912  fin1aufil  17966  hauspwpwf1  18021  ovolicc2lem4  19418  ovolioo  19464  i1fima2sn  19574  itg1addlem4  19593  itgsplitioo  19731  lhop1lem  19899  chordthmlem  20675  ressatans  20776  ftalem5  20861  ppiprm  20936  chtprm  20938  lgsdir2lem2  21110  dirith2  21224  ballotlemfp1  24751  ballotlem4  24758  ballotlemirc  24791  erdszelem8  24886  nodenselem7  25644  nobndup  25657  nobnddown  25658  axlowdimlem13  25895  axlowdim1  25900  nandsym1  26174  onsucsuccmpi  26195  onint1  26201  mblfinlem1  26245  mblfinlem2  26246  areacirclem4  26297  nn0prpwlem  26327  nn0prpw  26328  ivthALT  26340  prtlem90  26708  irrapx1  26893  stoweidlem35  27762  stirlinglem5  27805  sineq0ALT  29111  hdmaplem1  32631  hdmaplem2N  32632  hdmaplem3  32633
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator