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  4089  ovrcl  6126  tfi  6469  limom  6496  oaabs2  7089  ecexr  7111  elpmi  7236  elmapex  7238  pmresg  7245  pmsspw  7252  ixpssmap2g  7297  ixpssmapg  7298  resixpfo  7306  infensuc  7494  pm54.43lem  8174  alephnbtwn  8246  cfpwsdom  8753  elbasfv  14226  elbasov  14227  restsspw  14375  homarcl  14901  isipodrs  15336  grpidval  15437  efgrelexlema  16251  subcmn  16326  dvdsrval  16742  mvrf1  17503  pf1rcl  17788  elocv  18098  matrcl  18317  restrcl  18766  ssrest  18785  iscnp2  18848  isfcls  19587  isnghm  20307  dchrrcl  22584  eleenn  23147  hmdmadj  25349  indispcon  27128  cvmtop1  27154  cvmtop2  27155  dfon2lem7  27607  sltval2  27802  sltres  27810  funpartlem  27978  rankeq1o  28214  mapco2g  29055  atbase  32939  llnbase  33158  lplnbase  33183  lvolbase  33227  lhpbase  33647