Theorem nsyl2 121

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 119	1 |- ( ph -> ch )

Syntax hints:   -. wn 3   -> wi 4

This theorem is referenced by:  con1i  123  con4i  124  dvelimvOLD  1994  oprcl  3968  tfi  4792  limom  4819  ovrcl  6070  oaabs2  6847  ecexr  6869  elpmi  6994  elmapex  6996  pmresg  7000  pmsspw  7007  ixpssmap2g  7050  ixpssmapg  7051  resixpfo  7059  infensuc  7244  pm54.43lem  7842  alephnbtwn  7908  cfpwsdom  8415  elbasfv  13467  elbasov  13468  restsspw  13614  homarcl  14138  isipodrs  14542  grpidval  14662  efgrelexlema  15336  subcmn  15411  dvdsrval  15705  mvrf1  16444  elocv  16850  restrcl  17175  ssrest  17194  iscnp2  17257  isfcls  17994  isnghm  18710  pf1rcl  19922  dchrrcl  20977  hmdmadj  23396  indispcon  24874  cvmtop1  24900  cvmtop2  24901  dfon2lem7  25359  sltval2  25524  sltres  25532  funpartlem  25695  eleenn  25739  rankeq1o  26016  mapco2g  26659  matrcl  27334  dvelimvNEW7  29168  atbase  29772  llnbase  29991  lplnbase  30016  lvolbase  30060  lhpbase  30480

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8