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  4081  ovrcl  6120  tfi  6463  limom  6490  oaabs2  7080  ecexr  7102  elpmi  7227  elmapex  7229  pmresg  7236  pmsspw  7243  ixpssmap2g  7288  ixpssmapg  7289  resixpfo  7297  infensuc  7485  pm54.43lem  8165  alephnbtwn  8237  cfpwsdom  8744  elbasfv  14217  elbasov  14218  restsspw  14366  homarcl  14892  isipodrs  15327  grpidval  15428  efgrelexlema  16239  subcmn  16314  dvdsrval  16727  mvrf1  17476  pf1rcl  17752  elocv  18052  matrcl  18271  restrcl  18720  ssrest  18739  iscnp2  18802  isfcls  19541  isnghm  20261  dchrrcl  22538  eleenn  23077  hmdmadj  25279  indispcon  27053  cvmtop1  27079  cvmtop2  27080  dfon2lem7  27531  sltval2  27726  sltres  27734  funpartlem  27902  rankeq1o  28138  mapco2g  28975  atbase  32656  llnbase  32875  lplnbase  32900  lvolbase  32944  lhpbase  33364