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  900  intnanrd  901  intn3an1d  1321  intn3an2d  1322  intn3an3d  1323  ax10  2198  ax13fromc9  2207  camestres  2382  camestros  2386  calemes  2393  calemos  2396  pssn2lp  3445  sotrieq  4655  ordnbtwn  4796  funun  5448  canth  6036  dfwe2  6382  pwuninel2  6779  swoer  7117  swoord1  7118  swoord2  7119  php2  7484  en3lp  7810  cantnfp1lem1  7874  cantnfp1lem3  7876  cantnflem2  7886  cantnfp1lem1OLD  7900  cantnfp1lem3OLD  7902  rankxpsuc  8077  cardmin2  8156  infxpenlem  8168  cardaleph  8247  isfin4-3  8472  fin23lem24  8479  fin23lem25  8481  fin23lem26  8482  fin23lem38  8506  isfin32i  8522  fin34  8547  fin67  8552  nd3  8741  fpwwe2lem13  8797  canthnum  8804  canthwe  8806  pwfseq  8819  gchcdaidm  8823  gchxpidm  8824  winainflem  8848  r1wunlim  8892  suplem2pr  9210  elnnz  10644  fzneuz  11525  fzodisj  11567  hasheq0  12115  swrd0  12311  cnpart  12713  sqreulem  12831  rlimuni  13012  rlimcld2  13040  divalglem6  13585  bitsf1  13625  infpnlem1  13954  ramubcl  14062  ressress  14218  mreexmrid  14564  gsum2d  16437  gsum2dOLD  16438  dprddomprc  16456  ablfacrplem  16540  mplsubrglem  17451  mplsubrglemOLD  17452  mdetunilem6  18265  mdetunilem9  18268  madugsum  18291  infil  19278  fbasfip  19283  fgcl  19293  fin1aufil  19347  hauspwpwf1  19402  ovolicc2lem4  20845  ovolioo  20891  i1fima2sn  21000  itg1addlem4  21019  itgsplitioo  21157  lhop1lem  21327  chordthmlem  22112  ressatans  22214  ftalem5  22299  ppiprm  22374  chtprm  22376  lgsdir2lem2  22548  dirith2  22662  axlowdimlem13  23023  axlowdim1  23028  eulerpartlemgvv  26607  ballotlemfp1  26722  ballotlem4  26729  ballotlemirc  26762  erdszelem8  26934  nodenselem7  27675  nobndup  27688  nobnddown  27689  nandsym1  28116  onsucsuccmpi  28137  onint1  28143  fin2solem  28259  mblfinlem1  28272  mblfinlem2  28273  dvasin  28324  dvacos  28325  areacirclem4  28331  nn0prpwlem  28361  nn0prpw  28362  ivthALT  28374  prtlem90  28847  irrapx1  29014  stoweidlem35  29676  stirlinglem5  29719  frgra2v  30437  rng1nfld  30736  lmod1zrnlvec  30745  sineq0ALT  31375  hdmaplem1  34989  hdmaplem2N  34990  hdmaplem3  34991