Theorem nsyl 121

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

Step	Hyp	Ref	Expression
1		nsyl.1	. . 3 |- ( ph -> -. ps )
2		nsyl.2	. . 3 |- ( ch -> ps )
3	1, 2	nsyl3 119	. 2 |- ( ch -> -. ph )
4	3	con2i 120	1 |- ( ph -> -. ch )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  con3i  135  intnand  914  intnanrd  915  intn3an1d  1338  intn3an2d  1339  intn3an3d  1340  ax10  2219  ax13fromc9  2228  camestres  2413  camestros  2417  calemes  2424  calemos  2427  pssn2lp  3605  sotrieq  4827  ordnbtwn  4968  funun  5630  canth  6242  dfwe2  6601  pwuninel2  7003  swoer  7339  swoord1  7340  swoord2  7341  php2  7702  en3lp  8033  cantnfp1lem1  8097  cantnfp1lem3  8099  cantnflem2  8109  cantnfp1lem1OLD  8123  cantnfp1lem3OLD  8125  rankxpsuc  8300  cardmin2  8379  infxpenlem  8391  cardaleph  8470  isfin4-3  8695  fin23lem24  8702  fin23lem25  8704  fin23lem26  8705  fin23lem38  8729  isfin32i  8745  fin34  8770  fin67  8775  nd3  8964  fpwwe2lem13  9020  canthnum  9027  canthwe  9029  pwfseq  9042  gchcdaidm  9046  gchxpidm  9047  winainflem  9071  r1wunlim  9115  suplem2pr  9431  elnnz  10874  fzneuz  11759  fzodisj  11827  hasheq0  12401  swrd0  12621  cnpart  13036  sqreulem  13155  rlimuni  13336  rlimcld2  13364  divalglem6  13915  bitsf1  13955  infpnlem1  14287  ramubcl  14395  ressress  14552  mreexmrid  14898  gsum2d  16802  gsum2dOLD  16803  dprddomprc  16834  ablfacrplem  16918  rng1nfld  17725  mplsubrglem  17899  mplsubrglemOLD  17900  mdetunilem6  18914  mdetunilem9  18917  madugsum  18940  infil  20127  fbasfip  20132  fgcl  20142  fin1aufil  20196  hauspwpwf1  20251  ovolicc2lem4  21694  ovolioo  21741  i1fima2sn  21850  itg1addlem4  21869  itgsplitioo  22007  lhop1lem  22177  chordthmlem  22919  ressatans  23021  ftalem5  23106  ppiprm  23181  chtprm  23183  lgsdir2lem2  23355  dirith2  23469  axlowdimlem13  23961  axlowdim1  23966  frgra2v  24703  eulerpartlemgvv  27983  ballotlemfp1  28098  ballotlem4  28105  ballotlemirc  28138  erdszelem8  28310  nodenselem7  29052  nobndup  29065  nobnddown  29066  nandsym1  29492  onsucsuccmpi  29513  onint1  29519  fin2solem  29644  mblfinlem1  29656  mblfinlem2  29657  dvasin  29708  dvacos  29709  areacirclem4  29715  nn0prpwlem  29745  nn0prpw  29746  ivthALT  29758  prtlem90  30230  irrapx1  30396  cncfiooicclem1  31260  stoweidlem35  31363  stirlinglem5  31406  lmod1zrnlvec  32194  sineq0ALT  32835  hdmaplem1  36586  hdmaplem2N  36587  hdmaplem3  36588