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  914  intnanrd  915  intn3an1d  1336  intn3an2d  1337  intn3an3d  1338  ax10  2228  ax13fromc9  2237  camestres  2400  camestros  2404  calemes  2411  calemos  2414  pssn2lp  3591  sotrieq  4816  ordnbtwn  4957  funun  5612  canth  6229  dfwe2  6590  pwuninel2  6995  swoer  7331  swoord1  7332  swoord2  7333  php2  7695  en3lp  8024  cantnfp1lem1  8088  cantnfp1lem3  8090  cantnflem2  8100  cantnfp1lem1OLD  8114  cantnfp1lem3OLD  8116  rankxpsuc  8291  cardmin2  8370  infxpenlem  8382  cardaleph  8461  isfin4-3  8686  fin23lem24  8693  fin23lem25  8695  fin23lem26  8696  fin23lem38  8720  isfin32i  8736  fin34  8761  fin67  8766  nd3  8955  fpwwe2lem13  9009  canthnum  9016  canthwe  9018  pwfseq  9031  gchcdaidm  9035  gchxpidm  9036  r1wunlim  9104  suplem2pr  9420  elnnz  10870  fzneuz  11763  fzodisj  11836  hasheq0  12416  swrd0  12650  cnpart  13155  sqreulem  13274  rlimuni  13455  rlimcld2  13483  divalglem6  14140  bitsf1  14180  infpnlem1  14512  ramubcl  14620  ressress  14781  mreexmrid  15132  gsum2d  17195  gsum2dOLD  17196  dprddomprc  17226  ablfacrplem  17311  rng1nfld  18121  mplsubrglem  18295  mplsubrglemOLD  18296  mdetunilem6  19286  mdetunilem9  19289  madugsum  19312  infil  20530  fbasfip  20535  fgcl  20545  fin1aufil  20599  hauspwpwf1  20654  ovolicc2lem4  22097  ovolioo  22144  i1fima2sn  22253  itg1addlem4  22272  itgsplitioo  22410  lhop1lem  22580  chordthmlem  23360  ressatans  23462  ftalem5  23548  ppiprm  23623  chtprm  23625  lgsdir2lem2  23797  dirith2  23911  axlowdimlem13  24459  axlowdim1  24464  frgra2v  25201  eulerpartlemgvv  28579  ballotlemfp1  28694  ballotlem4  28701  ballotlemirc  28734  erdszelem8  28906  nodenselem7  29687  nobndup  29700  nobnddown  29701  nandsym1  30115  onsucsuccmpi  30136  onint1  30142  fin2solem  30279  mblfinlem1  30291  mblfinlem2  30292  dvasin  30343  dvacos  30344  areacirclem4  30350  nn0prpwlem  30380  nn0prpw  30381  ivthALT  30393  prtlem90  30838  irrapx1  31003  sumnnodd  31875  fperdvper  31954  stoweidlem35  32056  stirlinglem5  32099  fourierdlem68  32196  fourierswlem  32252  fouriersw  32253  zrninitoringc  33133  lmod1zrnlvec  33349  sineq0ALT  34138  hdmaplem1  37895  hdmaplem2N  37896  hdmaplem3  37897