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  927  intnanrd  928  intn3an1d  1379  intn3an2d  1380  intn3an3d  1381  camestres  2399  camestros  2403  calemes  2410  calemos  2413  pssn2lp  3534  sotrieq  4782  ordnbtwn  5513  funun  5624  canth  6249  dfwe2  6608  pwuninel2  7021  swoer  7391  swoord1  7392  swoord2  7393  php2  7757  en3lp  8121  cantnfp1lem1  8183  cantnfp1lem3  8185  cantnflem2  8195  rankxpsuc  8353  cardmin2  8432  infxpenlem  8444  cardaleph  8520  isfin4-3  8745  fin23lem24  8752  fin23lem25  8754  fin23lem26  8755  fin23lem38  8779  isfin32i  8795  fin34  8820  fin67  8825  nd3  9014  fpwwe2lem13  9067  canthnum  9074  canthwe  9076  pwfseq  9089  gchcdaidm  9093  gchxpidm  9094  r1wunlim  9162  suplem2pr  9478  elnnz  10947  fzneuz  11875  fzodisj  11952  hasheq0  12544  swrd0  12790  cnpart  13303  sqreulem  13422  rlimuni  13614  rlimcld2  13642  divalglem6  14378  bitsf1  14420  infpnlem1  14854  ramubcl  14976  ressress  15187  mreexmrid  15549  gsum2d  17604  dprddomprc  17632  ablfacrplem  17698  rng1nfld  18502  mplsubrglem  18663  mdetunilem6  19642  mdetunilem9  19645  madugsum  19668  infil  20878  fbasfip  20883  fgcl  20893  fin1aufil  20947  hauspwpwf1  21002  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  ovolioo  22521  i1fima2sn  22638  itg1addlem4  22657  itgsplitioo  22795  lhop1lem  22965  chordthmlem  23758  ressatans  23860  ftalem5  24001  ftalem5OLD  24003  ppiprm  24078  chtprm  24080  lgsdir2lem2  24252  dirith2  24366  axlowdimlem13  24984  axlowdim1  24989  frgra2v  25727  eulerpartlemgvv  29209  ballotlemfp1  29324  ballotlem4  29331  ballotlemirc  29364  ballotlemircOLD  29402  erdszelem8  29921  bccolsum  30375  nodenselem7  30576  nobndup  30589  nobnddown  30590  nn0prpwlem  30978  nn0prpw  30979  ivthALT  30991  nandsym1  31082  onsucsuccmpi  31103  onint1  31109  topdifinffinlem  31750  relowlssretop  31766  fin2solem  31931  poimirlem2  31942  poimirlem3  31943  poimirlem4  31944  poimirlem6  31946  poimirlem7  31947  poimirlem8  31948  poimirlem9  31949  poimirlem13  31953  poimirlem14  31954  poimirlem15  31955  poimirlem16  31956  poimirlem17  31957  poimirlem19  31959  poimirlem20  31960  poimirlem21  31961  poimirlem22  31962  poimirlem23  31963  poimirlem26  31966  poimirlem31  31971  mblfinlem1  31977  mblfinlem2  31978  dvasin  32028  dvacos  32029  areacirclem4  32035  prtlem90  32431  ax10  32467  ax13fromc9  32476  hdmaplem1  35339  hdmaplem2N  35340  hdmaplem3  35341  irrapx1  35672  sineq0ALT  37334  sumnnodd  37710  fperdvper  37790  stoweidlem35  37896  stirlinglem5  37940  fourierdlem68  38038  fourierswlem  38094  fouriersw  38095  opabn1stprc  39007  zrninitoringc  40126  lmod1zrnlvec  40340