Theorem nsyl 593

Description: A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)

Hypotheses

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

Assertion

Ref	Expression
nsyl	|- ( ph -> -. ch )

Proof of Theorem nsyl

Step	Hyp	Ref	Expression
1		nsyl.1	. . 3 |- ( ph -> -. ps )
2		nsyl.2	. . 3 |- ( ch -> ps )
3	1, 2	nsyl3 591	. 2 |- ( ch -> -. ph )
4	3	con2i 592	1 |- ( ph -> -. ch )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 579  ax-in2 580

This theorem is referenced by:  con3i  597  pm4.52im  841  intnand  878  intnanrd  879  camestres  2053  camestros  2057  calemes  2064  calemos  2067  unssin  3238  inssun  3239  onsucelsucexmid  4346  funun  5058  pwuninel2  6047  swoer  6318  swoord1  6319  swoord2  6320  ssfirab  6641  djune  6767  elnnz  8758  lbioog  9329  ubioog  9330  fzneuz  9511  fzodisj  9585  fxnn0nninf  9840  zfz1isolemiso  10240  infssuzex  11219