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  141  intnand  925  intnanrd  926  intn3an1d  1375  intn3an2d  1376  intn3an3d  1377  camestres  2369  camestros  2373  calemes  2380  calemos  2383  pssn2lp  3567  sotrieq  4799  ordnbtwn  5530  funun  5641  canth  6262  dfwe2  6620  pwuninel2  7027  swoer  7397  swoord1  7398  swoord2  7399  php2  7761  en3lp  8125  cantnfp1lem1  8186  cantnfp1lem3  8188  cantnflem2  8198  rankxpsuc  8356  cardmin2  8435  infxpenlem  8447  cardaleph  8522  isfin4-3  8747  fin23lem24  8754  fin23lem25  8756  fin23lem26  8757  fin23lem38  8781  isfin32i  8797  fin34  8822  fin67  8827  nd3  9016  fpwwe2lem13  9069  canthnum  9076  canthwe  9078  pwfseq  9091  gchcdaidm  9095  gchxpidm  9096  r1wunlim  9164  suplem2pr  9480  elnnz  10949  fzneuz  11877  fzodisj  11954  hasheq0  12545  swrd0  12786  cnpart  13297  sqreulem  13416  rlimuni  13607  rlimcld2  13635  divalglem6  14371  bitsf1  14413  infpnlem1  14847  ramubcl  14969  ressress  15180  mreexmrid  15542  gsum2d  17597  dprddomprc  17625  ablfacrplem  17691  rng1nfld  18495  mplsubrglem  18656  mdetunilem6  19634  mdetunilem9  19637  madugsum  19660  infil  20870  fbasfip  20875  fgcl  20885  fin1aufil  20939  hauspwpwf1  20994  ovolicc2lem4OLD  22465  ovolicc2lem4  22466  ovolioo  22513  i1fima2sn  22630  itg1addlem4  22649  itgsplitioo  22787  lhop1lem  22957  chordthmlem  23750  ressatans  23852  ftalem5  23993  ftalem5OLD  23995  ppiprm  24070  chtprm  24072  lgsdir2lem2  24244  dirith2  24358  axlowdimlem13  24976  axlowdim1  24981  frgra2v  25719  eulerpartlemgvv  29211  ballotlemfp1  29326  ballotlem4  29333  ballotlemirc  29366  ballotlemircOLD  29404  erdszelem8  29923  bccolsum  30376  nodenselem7  30575  nobndup  30588  nobnddown  30589  nn0prpwlem  30977  nn0prpw  30978  ivthALT  30990  nandsym1  31081  onsucsuccmpi  31102  onint1  31108  topdifinffinlem  31697  relowlssretop  31713  fin2solem  31851  poimirlem2  31862  poimirlem3  31863  poimirlem4  31864  poimirlem6  31866  poimirlem7  31867  poimirlem8  31868  poimirlem9  31869  poimirlem13  31873  poimirlem14  31874  poimirlem15  31875  poimirlem16  31876  poimirlem17  31877  poimirlem19  31879  poimirlem20  31880  poimirlem21  31881  poimirlem22  31882  poimirlem23  31883  poimirlem26  31886  poimirlem31  31891  mblfinlem1  31897  mblfinlem2  31898  dvasin  31948  dvacos  31949  areacirclem4  31955  prtlem90  32353  ax10  32392  ax13fromc9  32401  hdmaplem1  35264  hdmaplem2N  35265  hdmaplem3  35266  irrapx1  35598  sineq0ALT  37201  sumnnodd  37536  fperdvper  37616  stoweidlem35  37722  stirlinglem5  37766  fourierdlem68  37864  fourierswlem  37920  fouriersw  37921  zrninitoringc  39377  lmod1zrnlvec  39593