Theorem nsyl 637

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 635	. 2 |- ( ch -> -. ph )
4	3	con2i 636	1 |- ( ph -> -. ch )

This proof depends on syntax axioms:   -. wn 3   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used by:  con3i  641  pm4.52im  762  intnand  943  intnanrd  944  intn3an1d  1397  intn3an2d  1398  intn3an3d  1399  camestres  2192  camestros  2196  calemes  2203  calemos  2206  unssin  3470  inssun  3471  onsucelsucexmid  4677  funun  5422  opabn1stprc  6429  pwuninel2  6553  swoer  6835  swoord1  6836  swoord2  6837  ssfirab  7244  djune  7418  exmidaclem  7564  sucpw1nss3  7594  onntri35  7596  onntri45  7600  elnnz  9658  lbioog  10325  ubioog  10326  fzneuz  10518  fzodisj  10597  fzodisjsn  10601  infssuzex  10676  fxnn0nninf  10889  zfz1isolemiso  11305  swrd0g  11446  infpnlem1  13158  ballotfilemfp1  13280  ballotfilem4  13290  ballotfilemirc  13324  exmidunben  13366  ppiprm  16170  lgsdir2lem2  16246  2lgslem3  16318  vdegp1aid  16653