Theorem nsyl2 127

Description: A negated syllogism inference. (Contributed by NM, 26-Jun-1994.)

Hypotheses

Ref	Expression
nsyl2.1	|- ( ph -> -. ps )
nsyl2.2	|- ( -. ch -> ps )

Assertion

Ref	Expression
nsyl2	|- ( ph -> ch )

Proof of Theorem nsyl2

Step	Hyp	Ref	Expression
1		nsyl2.1	. 2 |- ( ph -> -. ps )
2		nsyl2.2	. . 3 |- ( -. ch -> ps )
3	2	a1i 11	. 2 |- ( ph -> ( -. ch -> ps ) )
4	1, 3	mt3d 125	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:  con1i  129  con4i  130  oprcl  4244  ovrcl  6329  tfi  6687  limom  6714  oaabs2  7312  ecexr  7334  elpmi  7456  elmapex  7458  pmresg  7465  pmsspw  7472  ixpssmap2g  7517  ixpssmapg  7518  resixpfo  7526  infensuc  7714  pm54.43lem  8397  alephnbtwn  8469  cfpwsdom  8976  elbasfv  14693  elbasov  14694  restsspw  14849  homarcl  15434  isipodrs  15918  grpidval  16014  efgrelexlema  16894  subcmn  16972  dvdsrval  17421  mvrf1  18208  pf1rcl  18512  elocv  18826  matrcl  19041  restrcl  19785  ssrest  19804  iscnp2  19867  isfcls  20636  isnghm  21356  dchrrcl  23641  eleenn  24326  hmdmadj  26986  indispcon  28876  cvmtop1  28902  cvmtop2  28903  mrsub0  29073  mrsubf  29074  mrsubccat  29075  mrsubcn  29076  mrsubco  29078  mrsubvrs  29079  msubf  29089  mclsrcl  29118  dfon2lem7  29438  sltval2  29633  sltres  29641  funpartlem  29797  rankeq1o  30033  mapco2g  30851  atbase  35157  llnbase  35376  lplnbase  35401  lvolbase  35445  lhpbase  35865