Theorem nsyli 155

Description: A negated syllogism inference. (Contributed by NM, 3-May-1994.)

Hypotheses

Ref	Expression
nsyli.1	|- ( ph -> ( ps -> ch ) )
nsyli.2	|- ( th -> -. ch )

Assertion

Ref	Expression
nsyli	|- ( ph -> ( th -> -. ps ) )

Proof of Theorem nsyli

Step	Hyp	Ref	Expression
1		nsyli.2	. 2 |- ( th -> -. ch )
2		nsyli.1	. . 3 |- ( ph -> ( ps -> ch ) )
3	2	con3d 148	. 2 |- ( ph -> ( -. ch -> -. ps ) )
4	1, 3	syl5 34	1 |- ( ph -> ( th -> -. ps ) )

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:  necon3ad  2807  tz7.7  5749  onssneli  5837  tz7.48-2  7537  tz7.49  7540  php  8144  nndomo  8154  elirrv  8504  setind  8610  zorn2lem3  9320  alephval2  9394  inar1  9597  dfon2lem6  31693  sltres  31815  finminlem  32312  onint1  32448  poimirlem4  33413  gneispace  38432