Theorem nsyl2 131

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 129	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  133  con4i  134  oprcl  4190  ovrcl  6321  tfi  6677  limom  6704  oaabs2  7343  ecexr  7365  elpmi  7487  elmapex  7489  pmresg  7496  pmsspw  7503  ixpssmap2g  7548  ixpssmapg  7549  resixpfo  7557  infensuc  7747  pm54.43lem  8430  alephnbtwn  8499  cfpwsdom  9006  elbasfv  15163  elbasov  15164  restsspw  15323  homarcl  15916  isipodrs  16400  grpidval  16496  efgrelexlema  17392  subcmn  17470  dvdsrval  17866  mvrf1  18642  pf1rcl  18930  elocv  19224  matrcl  19430  restrcl  20166  ssrest  20185  iscnp2  20248  isfcls  21017  isnghm  21721  isnghmOLD  21739  dchrrcl  24161  eleenn  24919  hmdmadj  27586  indispcon  29950  cvmtop1  29976  cvmtop2  29977  mrsub0  30147  mrsubf  30148  mrsubccat  30149  mrsubcn  30150  mrsubco  30152  mrsubvrs  30153  msubf  30163  mclsrcl  30192  dfon2lem7  30428  sltval2  30536  sltres  30544  funpartlem  30702  rankeq1o  30931  atbase  32849  llnbase  33068  lplnbase  33093  lvolbase  33137  lhpbase  33557  mapco2g  35550