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  907  intnanrd  908  intn3an1d  1328  intn3an2d  1329  intn3an3d  1330  ax10  2196  ax13fromc9  2205  camestres  2387  camestros  2391  calemes  2398  calemos  2401  pssn2lp  3452  sotrieq  4663  ordnbtwn  4804  funun  5455  canth  6044  dfwe2  6388  pwuninel2  6785  swoer  7121  swoord1  7122  swoord2  7123  php2  7488  en3lp  7814  cantnfp1lem1  7878  cantnfp1lem3  7880  cantnflem2  7890  cantnfp1lem1OLD  7904  cantnfp1lem3OLD  7906  rankxpsuc  8081  cardmin2  8160  infxpenlem  8172  cardaleph  8251  isfin4-3  8476  fin23lem24  8483  fin23lem25  8485  fin23lem26  8486  fin23lem38  8510  isfin32i  8526  fin34  8551  fin67  8556  nd3  8745  fpwwe2lem13  8801  canthnum  8808  canthwe  8810  pwfseq  8823  gchcdaidm  8827  gchxpidm  8828  winainflem  8852  r1wunlim  8896  suplem2pr  9214  elnnz  10648  fzneuz  11533  fzodisj  11575  hasheq0  12123  swrd0  12319  cnpart  12721  sqreulem  12839  rlimuni  13020  rlimcld2  13048  divalglem6  13594  bitsf1  13634  infpnlem1  13963  ramubcl  14071  ressress  14227  mreexmrid  14573  gsum2d  16451  gsum2dOLD  16452  dprddomprc  16470  ablfacrplem  16554  mplsubrglem  17494  mplsubrglemOLD  17495  mdetunilem6  18398  mdetunilem9  18401  madugsum  18424  infil  19411  fbasfip  19416  fgcl  19426  fin1aufil  19480  hauspwpwf1  19535  ovolicc2lem4  20978  ovolioo  21024  i1fima2sn  21133  itg1addlem4  21152  itgsplitioo  21290  lhop1lem  21460  chordthmlem  22202  ressatans  22304  ftalem5  22389  ppiprm  22464  chtprm  22466  lgsdir2lem2  22638  dirith2  22752  axlowdimlem13  23151  axlowdim1  23156  eulerpartlemgvv  26711  ballotlemfp1  26826  ballotlem4  26833  ballotlemirc  26866  erdszelem8  27038  nodenselem7  27779  nobndup  27792  nobnddown  27793  nandsym1  28220  onsucsuccmpi  28241  onint1  28247  fin2solem  28368  mblfinlem1  28381  mblfinlem2  28382  dvasin  28433  dvacos  28434  areacirclem4  28440  nn0prpwlem  28470  nn0prpw  28471  ivthALT  28483  prtlem90  28955  irrapx1  29122  stoweidlem35  29783  stirlinglem5  29826  frgra2v  30544  rng1nfld  30916  lmod1zrnlvec  30925  sineq0ALT  31560  hdmaplem1  35256  hdmaplem2N  35257  hdmaplem3  35258