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  4238  ovrcl  6312  tfi  6666  limom  6693  oaabs2  7291  ecexr  7313  elpmi  7434  elmapex  7436  pmresg  7443  pmsspw  7450  ixpssmap2g  7495  ixpssmapg  7496  resixpfo  7504  infensuc  7692  pm54.43lem  8376  alephnbtwn  8448  cfpwsdom  8955  elbasfv  14533  elbasov  14534  restsspw  14683  homarcl  15209  isipodrs  15644  grpidval  15745  efgrelexlema  16563  subcmn  16638  dvdsrval  17078  mvrf1  17852  pf1rcl  18156  elocv  18466  matrcl  18681  restrcl  19424  ssrest  19443  iscnp2  19506  isfcls  20245  isnghm  20965  dchrrcl  23243  eleenn  23875  hmdmadj  26535  indispcon  28319  cvmtop1  28345  cvmtop2  28346  dfon2lem7  28798  sltval2  28993  sltres  29001  funpartlem  29169  rankeq1o  29405  mapco2g  30250  atbase  34086  llnbase  34305  lplnbase  34330  lvolbase  34374  lhpbase  34794