Theorem nsyl2 142

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 140	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  144  con4iOLD  145  oprcl  4427  ovrcl  6686  tfi  7053  limom  7080  oaabs2  7725  ecexr  7747  elpmi  7876  elmapex  7878  pmresg  7885  pmsspw  7892  ixpssmap2g  7937  ixpssmapg  7938  resixpfo  7946  infensuc  8138  pm54.43lem  8825  alephnbtwn  8894  cfpwsdom  9406  elbasfv  15920  elbasov  15921  restsspw  16092  homarcl  16678  isipodrs  17161  grpidval  17260  efgrelexlema  18162  subcmn  18242  dvdsrval  18645  mvrf1  19425  pf1rcl  19713  elocv  20012  matrcl  20218  restrcl  20961  ssrest  20980  iscnp2  21043  isfcls  21813  isnghm  22527  dchrrcl  24965  eleenn  25776  hmdmadj  28799  indispconn  31216  cvmtop1  31242  cvmtop2  31243  mrsub0  31413  mrsubf  31414  mrsubccat  31415  mrsubcn  31416  mrsubco  31418  mrsubvrs  31419  msubf  31429  mclsrcl  31458  dfon2lem7  31694  sltval2  31809  sltres  31815  funpartlem  32049  rankeq1o  32278  atbase  34576  llnbase  34795  lplnbase  34820  lvolbase  34864  lhpbase  35284  mapco2g  37277