Theorem nsyl 125

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 123	. 2 |- ( ch -> -. ph )
4	3	con2i 124	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  142  intnand  930  intnanrd  931  intn3an1d  1407  intn3an2d  1408  intn3an3d  1409  camestres  2419  camestros  2423  calemes  2430  calemos  2433  pssn2lp  3520  sotrieq  4787  ordnbtwn  5520  funun  5631  canth  6267  dfwe2  6627  pwuninel2  7039  swoer  7409  swoord1  7410  swoord2  7411  php2  7775  en3lp  8139  cantnfp1lem1  8201  cantnfp1lem3  8203  cantnflem2  8213  rankxpsuc  8371  cardmin2  8450  infxpenlem  8462  cardaleph  8538  isfin4-3  8763  fin23lem24  8770  fin23lem25  8772  fin23lem26  8773  fin23lem38  8797  isfin32i  8813  fin34  8838  fin67  8843  nd3  9032  fpwwe2lem13  9085  canthnum  9092  canthwe  9094  pwfseq  9107  gchcdaidm  9111  gchxpidm  9112  r1wunlim  9180  suplem2pr  9496  elnnz  10971  fzneuz  11901  fzodisj  11979  fzodisjsn  11982  hasheq0  12582  swrd0  12844  cnpart  13380  sqreulem  13499  rlimuni  13691  rlimcld2  13719  divalglem6  14457  bitsf1  14499  infpnlem1  14933  ramubcl  15055  ressress  15265  mreexmrid  15627  gsum2d  17682  dprddomprc  17710  ablfacrplem  17776  rng1nfld  18579  mplsubrglem  18740  mdetunilem6  19719  mdetunilem9  19722  madugsum  19745  infil  20956  fbasfip  20961  fgcl  20971  fin1aufil  21025  hauspwpwf1  21080  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  ovolioo  22600  i1fima2sn  22717  itg1addlem4  22736  itgsplitioo  22874  lhop1lem  23044  chordthmlem  23837  ressatans  23939  ftalem5  24080  ftalem5OLD  24082  ppiprm  24157  chtprm  24159  lgsdir2lem2  24331  dirith2  24445  axlowdimlem13  25063  axlowdim1  25068  frgra2v  25806  eulerpartlemgvv  29282  ballotlemfp1  29397  ballotlem4  29404  ballotlemirc  29437  ballotlemircOLD  29475  erdszelem8  29993  bccolsum  30446  nodenselem7  30647  nobndup  30660  nobnddown  30661  nn0prpwlem  31049  nn0prpw  31050  ivthALT  31062  nandsym1  31153  onsucsuccmpi  31174  onint1  31180  topdifinffinlem  31820  relowlssretop  31836  fin2solem  31995  poimirlem2  32006  poimirlem3  32007  poimirlem4  32008  poimirlem6  32010  poimirlem7  32011  poimirlem8  32012  poimirlem9  32013  poimirlem13  32017  poimirlem14  32018  poimirlem15  32019  poimirlem16  32020  poimirlem17  32021  poimirlem19  32023  poimirlem20  32024  poimirlem21  32025  poimirlem22  32026  poimirlem23  32027  poimirlem26  32030  poimirlem31  32035  mblfinlem1  32041  mblfinlem2  32042  dvasin  32092  dvacos  32093  areacirclem4  32099  prtlem90  32495  ax10  32531  ax13fromc9  32540  hdmaplem1  35410  hdmaplem2N  35411  hdmaplem3  35412  irrapx1  35743  sineq0ALT  37397  sumnnodd  37807  fperdvper  37887  stoweidlem35  38008  stirlinglem5  38052  fourierdlem68  38150  fourierswlem  38206  fouriersw  38207  opabn1stprc  39153  zrninitoringc  40581  lmod1zrnlvec  40795