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  9654  lbioog  10315  ubioog  10316  fzneuz  10508  fzodisj  10587  fzodisjsn  10591  infssuzex  10666  fxnn0nninf  10876  zfz1isolemiso  11291  swrd0g  11432  infpnlem1  13138  ballotfilemfp1  13231  ballotfilem4  13241  ballotfilemirc  13275  exmidunben  13317  lgsdir2lem2  16148  2lgslem3  16220  vdegp1aid  16555