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  6558  swoer  6840  swoord1  6841  swoord2  6842  ssfirab  7250  djune  7424  exmidaclem  7570  sucpw1nss3  7600  onntri35  7602  onntri45  7606  elnnz  9663  lbioog  10331  ubioog  10332  fzneuz  10524  fzodisj  10603  fzodisjsn  10607  infssuzex  10682  fxnn0nninf  10896  zfz1isolemiso  11312  swrd0g  11453  infpnlem1  13166  ballotfilemfp1  13288  ballotfilem4  13298  ballotfilemirc  13332  exmidunben  13374  gsumresfi  14262  mvrf1fi  15219  ppiprm  16276  chtprm  16278  lgsdir2lem2  16370  2lgslem3  16442  vdegp1aid  16777