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  4679  funun  5425  opabn1stprc  6433  pwuninel2  6557  swoer  6839  swoord1  6840  swoord2  6841  ssfirab  7248  djune  7424  exmidaclem  7570  sucpw1nss3  7600  onntri35  7602  onntri45  7606  elnnz  9665  lbioog  10332  ubioog  10333  fzneuz  10525  fzodisj  10604  fzodisjsn  10608  infssuzex  10683  fxnn0nninf  10897  zfz1isolemiso  11313  swrd0g  11454  infpnlem1  13167  ballotfilemfp1  13289  ballotfilem4  13299  ballotfilemirc  13333  exmidunben  13375  gsumresfi  14263  ppiprm  16259  chtprm  16261  lgsdir2lem2  16353  2lgslem3  16425  vdegp1aid  16760