Theorem nsyl 135

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 133	. 2 |- ( ch -> -. ph )
4	3	con2i 134	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  150  intnand  962  intnanrd  963  intn3an1d  1442  intn3an2d  1443  intn3an3d  1444  camestres  2570  camestros  2574  calemes  2581  calemos  2584  pssn2lp  3708  sotrieq  5062  ordnbtwn  5816  ordnbtwnOLD  5817  funun  5932  canth  6608  dfwe2  6981  opabn1stprc  7228  pwuninel2  7400  swoer  7772  swoord1  7773  swoord2  7774  php2  8145  en3lp  8513  cantnfp1lem1  8575  cantnfp1lem3  8577  cantnflem2  8587  rankxpsuc  8745  cardmin2  8824  infxpenlem  8836  cardaleph  8912  isfin4-3  9137  fin23lem24  9144  fin23lem25  9146  fin23lem26  9147  fin23lem38  9171  isfin32i  9187  fin34  9212  fin67  9217  nd3  9411  fpwwe2lem13  9464  canthnum  9471  canthwe  9473  pwfseq  9486  gchcdaidm  9490  gchxpidm  9491  r1wunlim  9559  suplem2pr  9875  elnnz  11387  fzneuz  12421  fzodisj  12502  fzodisjsn  12505  hasheq0  13154  swrd0  13434  cnpart  13980  sqreulem  14099  rlimuni  14281  rlimcld2  14309  divalglem6  15121  bitsf1  15168  infpnlem1  15614  ramubcl  15722  ressress  15938  mreexmrid  16303  gsum2d  18371  dprddomprc  18399  ablfacrplem  18464  rng1nfld  19278  mplsubrglem  19439  mdetunilem6  20423  mdetunilem9  20426  madugsum  20449  infil  21667  fbasfip  21672  fgcl  21682  fin1aufil  21736  hauspwpwf1  21791  ovolicc2lem4  23288  ovolioo  23336  i1fima2sn  23447  itg1addlem4  23466  itgsplitioo  23604  lhop1lem  23776  chordthmlem  24559  ressatans  24661  ftalem5  24803  ppiprm  24877  chtprm  24879  lgsdir2lem2  25051  dirith2  25217  axlowdimlem13  25834  axlowdim1  25839  nfrgr2v  27136  eulerpartlemgvv  30438  ballotlemfp1  30553  ballotlem4  30560  ballotlemirc  30593  erdszelem8  31180  bccolsum  31625  noresle  31846  noetalem3  31865  nn0prpwlem  32317  nn0prpw  32318  ivthALT  32330  nandsym1  32421  onsucsuccmpi  32442  onint1  32448  topdifinffinlem  33195  relowlssretop  33211  fin2solem  33395  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem9  33418  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem23  33432  poimirlem26  33435  poimirlem31  33440  mblfinlem1  33446  mblfinlem2  33447  dvasin  33496  dvacos  33497  areacirclem4  33503  ax10fromc7  34180  hdmaplem1  37060  hdmaplem2N  37061  hdmaplem3  37062  irrapx1  37392  gneispace  38432  sineq0ALT  39173  sumnnodd  39862  fperdvper  40133  stoweidlem35  40252  stirlinglem5  40295  fourierdlem68  40391  fourierswlem  40447  fouriersw  40448  zrninitoringc  42071  lmod1zrnlvec  42283  elsetrecslem  42444