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  1337  intn3an2d  1338  intn3an3d  1339  ax10  2210  ax13fromc9  2219  camestres  2387  camestros  2391  calemes  2398  calemos  2401  pssn2lp  3587  sotrieq  4813  ordnbtwn  4954  funun  5616  canth  6235  dfwe2  6598  pwuninel2  7001  swoer  7337  swoord1  7338  swoord2  7339  php2  7700  en3lp  8031  cantnfp1lem1  8095  cantnfp1lem3  8097  cantnflem2  8107  cantnfp1lem1OLD  8121  cantnfp1lem3OLD  8123  rankxpsuc  8298  cardmin2  8377  infxpenlem  8389  cardaleph  8468  isfin4-3  8693  fin23lem24  8700  fin23lem25  8702  fin23lem26  8703  fin23lem38  8727  isfin32i  8743  fin34  8768  fin67  8773  nd3  8962  fpwwe2lem13  9018  canthnum  9025  canthwe  9027  pwfseq  9040  gchcdaidm  9044  gchxpidm  9045  r1wunlim  9113  suplem2pr  9429  elnnz  10875  fzneuz  11763  fzodisj  11833  hasheq0  12407  swrd0  12632  cnpart  13047  sqreulem  13166  rlimuni  13347  rlimcld2  13375  divalglem6  13928  bitsf1  13968  infpnlem1  14300  ramubcl  14408  ressress  14566  mreexmrid  14912  gsum2d  16868  gsum2dOLD  16869  dprddomprc  16900  ablfacrplem  16984  rng1nfld  17794  mplsubrglem  17968  mplsubrglemOLD  17969  mdetunilem6  18986  mdetunilem9  18989  madugsum  19012  infil  20230  fbasfip  20235  fgcl  20245  fin1aufil  20299  hauspwpwf1  20354  ovolicc2lem4  21797  ovolioo  21844  i1fima2sn  21953  itg1addlem4  21972  itgsplitioo  22110  lhop1lem  22280  chordthmlem  23028  ressatans  23130  ftalem5  23215  ppiprm  23290  chtprm  23292  lgsdir2lem2  23464  dirith2  23578  axlowdimlem13  24122  axlowdim1  24127  frgra2v  24864  eulerpartlemgvv  28181  ballotlemfp1  28296  ballotlem4  28303  ballotlemirc  28336  erdszelem8  28508  nodenselem7  29415  nobndup  29428  nobnddown  29429  nandsym1  29855  onsucsuccmpi  29876  onint1  29882  fin2solem  30007  mblfinlem1  30019  mblfinlem2  30020  dvasin  30071  dvacos  30072  areacirclem4  30078  nn0prpwlem  30108  nn0prpw  30109  ivthALT  30121  prtlem90  30566  irrapx1  30732  sumnnodd  31540  fperdvper  31615  stoweidlem35  31702  stirlinglem5  31745  fourierdlem68  31842  fourierswlem  31898  fouriersw  31899  lmod1zrnlvec  32805  sineq0ALT  33445  hdmaplem1  37200  hdmaplem2N  37201  hdmaplem3  37202