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  7419  exmidaclem  7565  sucpw1nss3  7595  onntri35  7597  onntri45  7601  elnnz  9659  lbioog  10326  ubioog  10327  fzneuz  10519  fzodisj  10598  fzodisjsn  10602  infssuzex  10677  fxnn0nninf  10891  zfz1isolemiso  11307  swrd0g  11448  infpnlem1  13161  ballotfilemfp1  13283  ballotfilem4  13293  ballotfilemirc  13327  exmidunben  13369  ppiprm  16220  chtprm  16222  lgsdir2lem2  16314  2lgslem3  16386  vdegp1aid  16721