Theorem nsyl2 130

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 128	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  132  con4i  133  oprcl  4215  ovrcl  6338  tfi  6694  limom  6721  oaabs2  7354  ecexr  7376  elpmi  7498  elmapex  7500  pmresg  7507  pmsspw  7514  ixpssmap2g  7559  ixpssmapg  7560  resixpfo  7568  infensuc  7756  pm54.43lem  8432  alephnbtwn  8500  cfpwsdom  9007  elbasfv  15133  elbasov  15134  restsspw  15289  homarcl  15874  isipodrs  16358  grpidval  16454  efgrelexlema  17334  subcmn  17412  dvdsrval  17808  mvrf1  18584  pf1rcl  18872  elocv  19162  matrcl  19368  restrcl  20104  ssrest  20123  iscnp2  20186  isfcls  20955  isnghm  21655  dchrrcl  24031  eleenn  24772  hmdmadj  27428  indispcon  29745  cvmtop1  29771  cvmtop2  29772  mrsub0  29942  mrsubf  29943  mrsubccat  29944  mrsubcn  29945  mrsubco  29947  mrsubvrs  29948  msubf  29958  mclsrcl  29987  dfon2lem7  30222  sltval2  30330  sltres  30338  funpartlem  30494  rankeq1o  30723  atbase  32563  llnbase  32782  lplnbase  32807  lvolbase  32851  lhpbase  33271  mapco2g  35264