Theorem nsyl 628

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 626	. 2 |- ( ch -> -. ph )
4	3	con2i 627	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-in1 614  ax-in2 615

This theorem is referenced by:  con3i  632  pm4.52im  750  intnand  931  intnanrd  932  camestres  2131  camestros  2135  calemes  2142  calemos  2145  unssin  3375  inssun  3376  onsucelsucexmid  4530  funun  5261  pwuninel2  6283  swoer  6563  swoord1  6564  swoord2  6565  ssfirab  6933  djune  7077  exmidaclem  7207  sucpw1nss3  7234  onntri35  7236  onntri45  7240  elnnz  9263  lbioog  9913  ubioog  9914  fzneuz  10101  fzodisj  10178  fxnn0nninf  10438  zfz1isolemiso  10819  infssuzex  11950  infpnlem1  12357  exmidunben  12427  lgsdir2lem2  14433