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 )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is referenced 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  4672  funun  5417  opabn1stprc  6419  pwuninel2  6543  swoer  6825  swoord1  6826  swoord2  6827  ssfirab  7234  djune  7408  exmidaclem  7554  sucpw1nss3  7584  onntri35  7586  onntri45  7590  elnnz  9633  lbioog  10294  ubioog  10295  fzneuz  10486  fzodisj  10565  fzodisjsn  10569  infssuzex  10644  fxnn0nninf  10854  zfz1isolemiso  11269  swrd0g  11410  infpnlem1  13116  ballotfilemfp1  13209  ballotfilem4  13219  ballotfilemirc  13253  exmidunben  13295  lgsdir2lem2  16062  2lgslem3  16134  vdegp1aid  16469