Theorem nsyl 115

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 113	. 2 |- ( ch -> -. ph )
4	3	con2i 114	1 |- ( ph -> -. ch )

Syntax hints:   -. wn 3   -> wi 4

This theorem is referenced by:  con3i  129  intnand  883  intnanrd  884  ax12OLD  1986  ax6  2197  ax12from12o  2206  camestres  2358  camestros  2362  calemes  2369  calemos  2372  pssn2lp  3408  sotrieq  4490  ordnbtwn  4631  dfwe2  4721  funun  5454  canth  6498  pwuninel2  6503  swoer  6892  swoord1  6893  swoord2  6894  php2  7251  cantnfp1lem1  7590  cantnfp1lem3  7592  cantnflem2  7602  en3lp  7628  rankxpsuc  7762  cardmin2  7841  infxpenlem  7851  cardaleph  7926  isfin4-3  8151  fin23lem24  8158  fin23lem25  8160  fin23lem26  8161  fin23lem38  8185  isfin32i  8201  fin34  8226  fin67  8231  nd3  8420  fpwwe2lem13  8473  canthnum  8480  canthwe  8482  pwfseq  8495  gchcdaidm  8499  gchxpidm  8500  winainflem  8524  r1wunlim  8568  suplem2pr  8886  elnnz  10248  fzneuz  11083  fzodisj  11122  hasheq0  11599  cnpart  12000  sqreulem  12118  rlimuni  12299  rlimcld2  12327  divalglem6  12873  bitsf1  12913  infpnlem1  13233  ramubcl  13341  ressress  13481  mreexmrid  13823  gsum2d  15501  ablfacrplem  15578  mplsubrglem  16457  infil  17848  fbasfip  17853  fgcl  17863  fin1aufil  17917  hauspwpwf1  17972  ovolicc2lem4  19369  ovolioo  19415  i1fima2sn  19525  itg1addlem4  19544  itgsplitioo  19682  lhop1lem  19850  chordthmlem  20626  ressatans  20727  ftalem5  20812  ppiprm  20887  chtprm  20889  lgsdir2lem2  21061  dirith2  21175  ballotlemfp1  24702  ballotlem4  24709  ballotlemirc  24742  erdszelem8  24837  nodenselem7  25555  nobndup  25568  nobnddown  25569  axlowdimlem13  25797  axlowdim1  25802  nandsym1  26076  onsucsuccmpi  26097  onint1  26103  mblfinlem  26143  areacirclem5  26185  nn0prpwlem  26215  nn0prpw  26216  ivthALT  26228  prtlem90  26596  irrapx1  26781  stoweidlem35  27651  stirlinglem5  27694  hdmaplem1  32254  hdmaplem2N  32255  hdmaplem3  32256

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